Merge PR #7177: Unifying names of "smart" combinators + adding combinators in CArray

3 files changed, 20 insertions, 20 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2fe930dca..e1d2cf6d1 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -231,7 +231,7 @@ let rec map_kn f f' c =
 	  in
 	  let p' = func p in
 	  let ct' = func ct in
-	  let l' = Array.smartmap func l in
+          let l' = Array.Smart.map func l in
 	    if (ci.ci_ind==ci_ind && p'==p
 		&& l'==l && ct'==ct)then c
 	    else
@@ -260,21 +260,21 @@ let rec map_kn f f' c =
 	    else LetIn (na, b', t', ct')
       | App (ct,l) ->
 	  let ct' = func ct in
-	  let l' = Array.smartmap func l in
+          let l' = Array.Smart.map func l in
 	    if (ct'== ct && l'==l) then c
 	    else App (ct',l')
       | Evar (e,l) ->
-	  let l' = Array.smartmap func l in
+          let l' = Array.Smart.map func l in
 	    if (l'==l) then c
 	    else Evar (e,l')
       | Fix (ln,(lna,tl,bl)) ->
-	  let tl' = Array.smartmap func tl in
-	  let bl' = Array.smartmap func bl in
+          let tl' = Array.Smart.map func tl in
+          let bl' = Array.Smart.map func bl in
 	    if (bl == bl'&& tl == tl') then c
 	    else Fix (ln,(lna,tl',bl'))
       | CoFix(ln,(lna,tl,bl)) ->
-	  let tl' = Array.smartmap func tl in
-	  let bl' = Array.smartmap func bl in
+          let tl' = Array.Smart.map func tl in
+          let bl' = Array.Smart.map func bl in
 	    if (bl == bl'&& tl == tl') then c
 	    else CoFix (ln,(lna,tl',bl'))
       | _ -> c
@@ -480,7 +480,7 @@ let dest_subterms p =
   let (_,cstrs) = Rtree.dest_node p in
   Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
 
-let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
+let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p
 
 let eq_recarg r1 r2 = match r1, r2 with
   | Norec, Norec -> true
@@ -513,7 +513,7 @@ let subst_decl_arity f g sub ar =
 let subst_rel_declaration sub =
   Term.map_rel_decl (subst_mps sub)
 
-let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
+let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub)
 
 let constant_is_polymorphic cb =
   match cb.const_universes with
@@ -544,10 +544,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;
@@ -560,7 +560,7 @@ let subst_mind_packet sub mbp =
 let subst_mind sub mib =
   { mib with
     mind_params_ctxt = map_rel_context (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 }
 
 (* Modules *)
 
@@ -599,7 +599,7 @@ and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generi
     mod_mp = subst_mp sub mb.mod_mp;
     mod_expr = subst_impl sub mb.mod_expr;
     mod_type = subst_signature sub mb.mod_type;
-    mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg }
+    mod_type_alg = Option.Smart.map (subst_expression sub) mb.mod_type_alg }
 
 and subst_module sub mb =
   subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb
diff --git a/checker/term.ml b/checker/term.ml
index 0236f7867..509634bdb 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -243,7 +243,7 @@ let map_rel_decl f = function
        LocalDef (n, body', typ')
 
 let map_rel_context f =
-  List.smartmap (map_rel_decl f)
+  List.Smart.map (map_rel_decl f)
 
 let extended_rel_list n hyps =
   let rec reln l p = function
diff --git a/checker/univ.ml b/checker/univ.ml
index 7d285b6fe..15673736f 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -314,7 +314,7 @@ struct
 
   let for_all = List.for_all
 
-  let smartmap = List.smartmap
+  let smart_map = List.Smart.map
 
 end
 
@@ -911,12 +911,12 @@ struct
   let is_empty x = Int.equal (Array.length x) 0
 
   let subst_fn fn t = 
-    let t' = CArray.smartmap fn t in
+    let t' = CArray.Smart.map fn t in
       if t' == t then t else t'
 
   let subst s t =
     let t' = 
-      CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
+      CArray.Smart.map (fun x -> try LMap.find x s with Not_found -> x) t
     in if t' == t then t else t'
 
   let pr =
@@ -952,11 +952,11 @@ let subst_instance_level s l =
   | _ -> l
 
 let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
+  Array.Smart.map (fun l -> subst_instance_level s l) i
 
 let subst_instance_universe s u =
   let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
+  let u' = Universe.smart_map f u in
     if u == u' then u
     else Universe.sort u'
 
@@ -1097,7 +1097,7 @@ let subst_univs_level_level subst l =
 
 let subst_univs_level_universe subst u =
   let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
-  let u' = Universe.smartmap f u in
+  let u' = Universe.smart_map f u in
     if u == u' then u
     else Universe.sort u'