Collecting Array.smart_* functions into a module Array.Smart.

1 files changed, 9 insertions, 9 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3652a1ce4..90a6eb6f7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -198,10 +198,10 @@ let subst_mind_packet sub mbp =
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_consnrealargs = mbp.mind_consnrealargs;
     mind_typename = mbp.mind_typename;
-    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
+    mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
     mind_arity = subst_ind_arity sub mbp.mind_arity;
-    mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
+    mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_nrealdecls = mbp.mind_nrealdecls;
     mind_kelim = mbp.mind_kelim;
@@ -211,8 +211,8 @@ let subst_mind_packet sub mbp =
     mind_reloc_tbl = mbp.mind_reloc_tbl }
 
 let subst_mind_record sub (id, ps, pb as r) =
-  let ps' = Array.smartmap (subst_constant sub) ps in
-  let pb' = Array.smartmap (subst_const_proj sub) pb in
+  let ps' = Array.Smart.map (subst_constant sub) ps in
+  let pb' = Array.Smart.map (subst_const_proj sub) pb in
     if ps' == ps && pb' == pb then r
     else (id, ps', pb')
 
@@ -225,7 +225,7 @@ let subst_mind_body sub mib =
     mind_nparams_rec = mib.mind_nparams_rec;
     mind_params_ctxt =
       Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
-    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
+    mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
@@ -263,15 +263,15 @@ let hcons_ind_arity =
 (** Substitution of inductive declarations *)
 
 let hcons_mind_packet oib =
-  let user = Array.smartmap Constr.hcons oib.mind_user_lc in
-  let nf = Array.smartmap Constr.hcons oib.mind_nf_lc in
+  let user = Array.Smart.map Constr.hcons oib.mind_user_lc in
+  let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in
   (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *)
   let nf = if Array.equal (==) user nf then user else nf in
   { oib with
     mind_typename = Names.Id.hcons oib.mind_typename;
     mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
     mind_arity = hcons_ind_arity oib.mind_arity;
-    mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
+    mind_consnames = Array.Smart.map Names.Id.hcons oib.mind_consnames;
     mind_user_lc = user;
     mind_nf_lc = nf }
 
@@ -283,7 +283,7 @@ let hcons_mind_universes miu =
 
 let hcons_mind mib =
   { mib with
-    mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
+    mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_universes = hcons_mind_universes mib.mind_universes }