aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/himsg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/himsg.ml')
-rw-r--r--vernac/himsg.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 3c4fcf714..1add1f486 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -86,7 +86,7 @@ let j_nf_betaiotaevar env sigma j =
uj_type = Reductionops.nf_betaiota env sigma j.uj_type }
let jv_nf_betaiotaevar env sigma jl =
- Array.map (fun j -> j_nf_betaiotaevar env sigma j) jl
+ Array.Smart.map (fun j -> j_nf_betaiotaevar env sigma j) jl
(** Printers *)