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

7 files changed, 44 insertions, 44 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 56e5828918..7795084779 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -920,7 +920,7 @@ let rec subst_cases_pattern subst = DAst.map (function
   | PatVar _ as pat -> pat
   | PatCstr (((kn,i),j),cpl,n) as pat ->
       let kn' = subst_mind subst kn
-      and cpl' = List.smartmap (subst_cases_pattern subst) cpl in
+      and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (((kn',i),j),cpl',n)
   )
@@ -940,7 +940,7 @@ let rec subst_glob_constr subst = DAst.map (function
 
   | GApp (r,rl) as raw ->
       let r' = subst_glob_constr subst r
-      and rl' = List.smartmap (subst_glob_constr subst) rl in
+      and rl' = List.Smart.map (subst_glob_constr subst) rl in
 	if r' == r && rl' == rl then raw else
 	  GApp(r',rl')
 
@@ -957,25 +957,25 @@ let rec subst_glob_constr subst = DAst.map (function
   | GLetIn (n,r1,t,r2) as raw ->
       let r1' = subst_glob_constr subst r1 in
       let r2' = subst_glob_constr subst r2 in
-      let t' = Option.smartmap (subst_glob_constr subst) t in
+      let t' = Option.Smart.map (subst_glob_constr subst) t in
 	if r1' == r1 && t == t' && r2' == r2 then raw else
 	  GLetIn (n,r1',t',r2')
 
   | GCases (sty,rtno,rl,branches) as raw ->
     let open CAst in
-      let rtno' = Option.smartmap (subst_glob_constr subst) rtno
-      and rl' = List.smartmap (fun (a,x as y) ->
+      let rtno' = Option.Smart.map (subst_glob_constr subst) rtno
+      and rl' = List.Smart.map (fun (a,x as y) ->
         let a' = subst_glob_constr subst a in
         let (n,topt) = x in
-        let topt' = Option.smartmap
+        let topt' = Option.Smart.map
           (fun ({loc;v=((sp,i),y)} as t) ->
             let sp' = subst_mind subst sp in
             if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
-      and branches' = List.smartmap
+      and branches' = List.Smart.map
                         (fun ({loc;v=(idl,cpl,r)} as branch) ->
 			   let cpl' =
-			     List.smartmap (subst_cases_pattern subst) cpl
+                             List.Smart.map (subst_cases_pattern subst) cpl
 			   and r' = subst_glob_constr subst r in
 			     if cpl' == cpl && r' == r then branch else
                                CAst.(make ?loc (idl,cpl',r')))
@@ -985,14 +985,14 @@ let rec subst_glob_constr subst = DAst.map (function
 	  GCases (sty,rtno',rl',branches')
 
   | GLetTuple (nal,(na,po),b,c) as raw ->
-      let po' = Option.smartmap (subst_glob_constr subst) po
+      let po' = Option.Smart.map (subst_glob_constr subst) po
       and b' = subst_glob_constr subst b
       and c' = subst_glob_constr subst c in
 	if po' == po && b' == b && c' == c then raw else
           GLetTuple (nal,(na,po'),b',c')
 
   | GIf (c,(na,po),b1,b2) as raw ->
-      let po' = Option.smartmap (subst_glob_constr subst) po
+      let po' = Option.Smart.map (subst_glob_constr subst) po
       and b1' = subst_glob_constr subst b1
       and b2' = subst_glob_constr subst b2
       and c' = subst_glob_constr subst c in
@@ -1000,12 +1000,12 @@ let rec subst_glob_constr subst = DAst.map (function
           GIf (c',(na,po'),b1',b2')
 
   | GRec (fix,ida,bl,ra1,ra2) as raw ->
-      let ra1' = Array.smartmap (subst_glob_constr subst) ra1
-      and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in
-      let bl' = Array.smartmap
-        (List.smartmap (fun (na,k,obd,ty as dcl) ->
+      let ra1' = Array.Smart.map (subst_glob_constr subst) ra1
+      and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in
+      let bl' = Array.Smart.map
+        (List.Smart.map (fun (na,k,obd,ty as dcl) ->
           let ty' = subst_glob_constr subst ty in
-          let obd' = Option.smartmap (subst_glob_constr subst) obd in
+          let obd' = Option.Smart.map (subst_glob_constr subst) obd in
           if ty'==ty && obd'==obd then dcl else (na,k,obd',ty')))
         bl in
 	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
@@ -1018,7 +1018,7 @@ let rec subst_glob_constr subst = DAst.map (function
       if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
     | _ -> knd
     in
-    let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in
+    let nsolve = Option.Smart.map (Hook.get f_subst_genarg subst) solve in
     if nsolve == solve && nknd == knd then raw
     else GHole (nknd, naming, nsolve)
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 3ae04cd4fa..5056c0457e 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -331,19 +331,19 @@ let bound_glob_vars =
 
 (** Mapping of names in binders *)
 
-(* spiwack: I used a smartmap-style kind of mapping here, because the
+(* spiwack: I used a smart-style kind of mapping here, because the
    operation will be the identity almost all of the time (with any
    term outside of Ltac to begin with). But to be honest, there would
    probably be no significant penalty in doing reallocation as
    pattern-matching expressions are usually rather small. *)
 
 let map_inpattern_binders f ({loc;v=(id,nal)} as x) =
-  let r = CList.smartmap f nal in
+  let r = CList.Smart.map f nal in
   if r == nal then x
   else CAst.make ?loc (id,r)
 
 let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple =
-  let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in
+  let r = Option.Smart.map (fun p -> map_inpattern_binders f p) inp in
   if r == inp then x
   else c,(f na, r)
 
@@ -355,7 +355,7 @@ let rec map_case_pattern_binders f = DAst.map (function
   | PatCstr (c,ps,na) as x ->
       let rna = f na in
       let rps =
-        CList.smartmap (fun p -> map_case_pattern_binders f p) ps
+        CList.Smart.map (fun p -> map_case_pattern_binders f p) ps
       in
       if rna == na && rps == ps then x
       else PatCstr(c,rps,rna)
@@ -366,13 +366,13 @@ let map_cases_branch_binders f ({CAst.loc;v=(il,cll,rhs)} as x) : cases_clause =
      It is intended to be a superset of the free variable of the
      right-hand side, if I understand correctly. But I'm not sure when
      or how they are used. *)
-  let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in
+  let r = List.Smart.map (fun cl -> map_case_pattern_binders f cl) cll in
   if r == cll then x
   else CAst.make ?loc (il,r,rhs)
 
 let map_pattern_binders f tomatch branches =
-  CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch,
-  CList.smartmap (fun br -> map_cases_branch_binders f br) branches
+  CList.Smart.map (fun tm -> map_tomatch_binders f tm) tomatch,
+  CList.Smart.map (fun br -> map_cases_branch_binders f br) branches
 
 (** /mapping of names in binders *)
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ccfb7f9900..375ed10d0d 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -293,11 +293,11 @@ let rec subst_pattern subst pat =
 	  PProj(p',c')
   | PApp (f,args) ->
       let f' = subst_pattern subst f in
-      let args' = Array.smartmap (subst_pattern subst) args in
+      let args' = Array.Smart.map (subst_pattern subst) args in
 	if f' == f && args' == args then pat else
 	  PApp (f',args')
   | PSoApp (i,args) ->
-      let args' = List.smartmap (subst_pattern subst) args in
+      let args' = List.Smart.map (subst_pattern subst) args in
 	if args' == args then pat else
 	  PSoApp (i,args')
   | PLambda (name,c1,c2) ->
@@ -312,7 +312,7 @@ let rec subst_pattern subst pat =
 	  PProd (name,c1',c2')
   | PLetIn (name,c1,t,c2) ->
       let c1' = subst_pattern subst c1 in
-      let t' = Option.smartmap (subst_pattern subst) t in
+      let t' = Option.Smart.map (subst_pattern subst) t in
       let c2' = subst_pattern subst c2 in
 	if c1' == c1 && t' == t && c2' == c2 then pat else
 	  PLetIn (name,c1',t',c2')
@@ -326,7 +326,7 @@ let rec subst_pattern subst pat =
 	  PIf (c',c1',c2')
   | PCase (cip,typ,c,branches) ->
       let ind = cip.cip_ind in
-      let ind' = Option.smartmap (subst_ind subst) ind in
+      let ind' = Option.Smart.map (subst_ind subst) ind in
       let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in
       let typ' = subst_pattern subst typ in
       let c' = subst_pattern subst c in
@@ -334,18 +334,18 @@ let rec subst_pattern subst pat =
 	let c' = subst_pattern subst c in
 	if c' == c then br else (i,n,c')
       in
-      let branches' = List.smartmap subst_branch branches in
+      let branches' = List.Smart.map subst_branch branches in
       if cip' == cip && typ' == typ && c' == c && branches' == branches
       then pat
       else PCase(cip', typ', c', branches')
   | PFix (lni,(lna,tl,bl)) ->
-      let tl' = Array.smartmap (subst_pattern subst) tl in
-      let bl' = Array.smartmap (subst_pattern subst) bl in
+      let tl' = Array.Smart.map (subst_pattern subst) tl in
+      let bl' = Array.Smart.map (subst_pattern subst) bl in
       if bl' == bl && tl' == tl then pat
       else PFix (lni,(lna,tl',bl'))
   | PCoFix (ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap (subst_pattern subst) tl in
-      let bl' = Array.smartmap (subst_pattern subst) bl in
+      let tl' = Array.Smart.map (subst_pattern subst) tl in
+      let bl' = Array.Smart.map (subst_pattern subst) bl in
       if bl' == bl && tl' == tl then pat
       else PCoFix (ln,(lna,tl',bl'))
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6bf852fcd9..de72f94272 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -421,7 +421,7 @@ let ltac_interp_name_env k0 lvar env sigma =
   let n = Context.Rel.length (rel_context env) - k0 in
   let ctxt,_ = List.chop n (rel_context env) in
   let open Context.Rel.Declaration in
-  let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in
+  let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in
   if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
   else push_rel_context sigma ctxt' (pop_rel_context n env sigma)
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 84aceeedd4..9eb410f06a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -69,8 +69,8 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
   let projs' =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
-   List.smartmap
-     (Option.smartmap (fun kn -> fst (subst_con_kn subst kn)))
+   List.Smart.map
+     (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn)))
     projs
   in
   let id' = fst (subst_constructor subst id) in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 34d7a07984..6fde868370 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1404,7 +1404,7 @@ let plain_instance sigma s c =
     | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
     | App (f,l) when isCast sigma f ->
         let (f,_,t) = destCast sigma f in
-        let l' = CArray.Fun1.smartmap irec n l in
+        let l' = Array.Fun1.Smart.map irec n l in
         (match EConstr.kind sigma f with
         | Meta p ->
 	    (* Don't flatten application nodes: this is used to extract a
@@ -1413,7 +1413,7 @@ let plain_instance sigma s c =
 	    (try let g = Metamap.find p s in
 	    match EConstr.kind sigma g with
             | App _ ->
-                let l' = CArray.Fun1.smartmap lift 1 l' in
+                let l' = Array.Fun1.Smart.map lift 1 l' in
                 mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l'))
             | _ -> mkApp (g,l')
 	    with Not_found -> mkApp (f,l'))
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 11cc6c1f00..12a944d322 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -180,12 +180,12 @@ let subst_class (subst,cl) =
   let do_subst_con c = Mod_subst.subst_constant subst c
   and do_subst c = Mod_subst.subst_mps subst c
   and do_subst_gr gr = fst (subst_global subst gr) in
-  let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in
+  let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in
   let do_subst_context (grs,ctx) =
-    List.smartmap (Option.smartmap do_subst_gr) grs,
+    List.Smart.map (Option.Smart.map do_subst_gr) grs,
     do_subst_ctx ctx in
-  let do_subst_projs projs = List.smartmap (fun (x, y, z) -> 
-    (x, y, Option.smartmap do_subst_con z)) projs in
+  let do_subst_projs projs = List.Smart.map (fun (x, y, z) ->
+    (x, y, Option.Smart.map do_subst_con z)) projs in
   { cl_univs = cl.cl_univs;
     cl_impl = do_subst_gr cl.cl_impl;
     cl_context = do_subst_context cl.cl_context;
@@ -223,7 +223,7 @@ let discharge_class (_,cl) =
                              | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
 			    ctx'
       in
-      List.smartmap (Option.smartmap Lib.discharge_global) grs
+      List.Smart.map (Option.Smart.map Lib.discharge_global) grs
       @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
@@ -234,12 +234,12 @@ let discharge_class (_,cl) =
     let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
     let context = discharge_context ctx (subst, usubst) cl.cl_context in
     let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
-    let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in
+    let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in
       { cl_univs = cl_univs';
         cl_impl = cl_impl';
 	cl_context = context;
 	cl_props = props;
-	cl_projs = List.smartmap discharge_proj cl.cl_projs;
+        cl_projs = List.Smart.map discharge_proj cl.cl_projs;
 	cl_strict = cl.cl_strict;
 	cl_unique = cl.cl_unique
       }