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

4 files changed, 11 insertions, 11 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 56e5828918..ea2889dea9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -1000,9 +1000,9 @@ 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
+      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.smartmap (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
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 3ae04cd4fa..95f02dceb0 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -331,7 +331,7 @@ 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
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ccfb7f9900..bc7ed6137f 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -293,7 +293,7 @@ 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) ->
@@ -339,13 +339,13 @@ let rec subst_pattern subst pat =
       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/reductionops.ml b/pretyping/reductionops.ml
index 34d7a07984..e07ed77117 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' = CArray.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' = CArray.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'))