23 files changed, 334 insertions, 290 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2fe930dca..ca31e143f 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
@@ -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 *)
 
diff --git a/checker/univ.ml b/checker/univ.ml
index 7d285b6fe..d3eab8613 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -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,7 +952,7 @@ 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
diff --git a/clib/cArray.ml b/clib/cArray.ml
index c1013dff4..6ea46655f 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -50,9 +50,9 @@ sig
   val map_of_list : ('a -> 'b) -> 'a list -> 'b array
   val chop : int -> 'a array -> 'a array * 'a array
   val smartmap : ('a -> 'a) -> 'a array -> 'a array
-  val smartmap2 : ('a -> 'b -> 'b) -> 'a array -> 'b array -> 'b array
+  [@@ocaml.deprecated "Same as [Smart.map]"]
   val smartfoldmap : ('r -> 'a -> 'r * 'a) -> 'r -> 'a array -> 'r * 'a array
-  val smartfoldmap2 : ('r -> 'a -> 'b -> 'r * 'b) -> 'r -> 'a array -> 'b array -> 'r * 'b array
+  [@@ocaml.deprecated "Same as [Smart.fold_left_map]"]
   val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map3 :
@@ -74,6 +74,13 @@ sig
   val rev_of_list : 'a list -> 'a array
   val rev_to_list : 'a array -> 'a list
   val filter_with : bool list -> 'a array -> 'a array
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a array -> 'a array
+    val map2 : ('a -> 'b -> 'b) -> 'a array -> 'b array -> 'b array
+    val fold_left_map : ('a -> 'b -> 'a * 'b) -> 'a -> 'b array -> 'a * 'b array
+    val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'c) -> 'a -> 'b array -> 'c array -> 'a * 'c array
+  end
 end
 
 include Array
@@ -328,142 +335,6 @@ let chop n v =
   if n > vlen then failwith "Array.chop";
   (Array.sub v 0 n, Array.sub v n (vlen-n))
 
-(* If none of the elements is changed by f we return ar itself.
-   The while loop looks for the first such an element.
-   If found, we break here and the new array is produced,
-   but f is not re-applied to elements that are already checked *)
-let smartmap f (ar : 'a array) =
-  let len = Array.length ar in
-  let i = ref 0 in
-  let break = ref true in
-  let temp = ref None in
-  while !break && (!i < len) do
-    let v = Array.unsafe_get ar !i in
-    let v' = f v in
-    if v == v' then incr i
-    else begin
-      break := false;
-      temp := Some v';
-    end
-  done;
-  if !i < len then begin
-    (** The array is not the same as the original one *)
-    let ans : 'a array = Array.copy ar in
-    let v = match !temp with None -> assert false | Some x -> x in
-    Array.unsafe_set ans !i v;
-    incr i;
-    while !i < len do
-      let v = Array.unsafe_get ans !i in
-      let v' = f v in
-      if v != v' then Array.unsafe_set ans !i v';
-      incr i
-    done;
-    ans
-  end else ar
-
-let smartmap2 f aux_ar ar =
-  let len = Array.length ar in
-  let aux_len = Array.length aux_ar in
-  let () = if not (Int.equal len aux_len) then invalid_arg "Array.smartmap2" in
-  let i = ref 0 in
-  let break = ref true in
-  let temp = ref None in
-  while !break && (!i < len) do
-    let v = Array.unsafe_get ar !i in
-    let w = Array.unsafe_get aux_ar !i in
-    let v' = f w v in
-    if v == v' then incr i
-    else begin
-      break := false;
-      temp := Some v';
-    end
-  done;
-  if !i < len then begin
-    (** The array is not the same as the original one *)
-    let ans : 'a array = Array.copy ar in
-    let v = match !temp with None -> assert false | Some x -> x in
-    Array.unsafe_set ans !i v;
-    incr i;
-    while !i < len do
-      let v = Array.unsafe_get ans !i in
-      let w = Array.unsafe_get aux_ar !i in
-      let v' = f w v in
-      if v != v' then Array.unsafe_set ans !i v';
-      incr i
-    done;
-    ans
-  end else ar
-
-(** Same as [smartmap] but threads a state meanwhile *)
-let smartfoldmap f accu (ar : 'a array) =
-  let len = Array.length ar in
-  let i = ref 0 in
-  let break = ref true in
-  let r = ref accu in
-  (** This variable is never accessed unset *)
-  let temp = ref None in
-  while !break && (!i < len) do
-    let v = Array.unsafe_get ar !i in
-    let (accu, v') = f !r v in
-    r := accu;
-    if v == v' then incr i
-    else begin
-      break := false;
-      temp := Some v';
-    end
-  done;
-  if !i < len then begin
-    let ans : 'a array = Array.copy ar in
-    let v = match !temp with None -> assert false | Some x -> x in
-    Array.unsafe_set ans !i v;
-    incr i;
-    while !i < len do
-      let v = Array.unsafe_get ar !i in
-      let (accu, v') = f !r v in
-      r := accu;
-      if v != v' then Array.unsafe_set ans !i v';
-      incr i
-    done;
-    !r, ans
-  end else !r, ar
-
-(** Same as [smartmap2] but threads a state meanwhile *)
-let smartfoldmap2 f accu aux_ar ar =
-  let len = Array.length ar in
-  let aux_len = Array.length aux_ar in
-  let () = if not (Int.equal len aux_len) then invalid_arg "Array.smartfoldmap2" in
-  let i = ref 0 in
-  let break = ref true in
-  let r = ref accu in
-  (** This variable is never accessed unset *)
-  let temp = ref None in
-  while !break && (!i < len) do
-    let v = Array.unsafe_get ar !i in
-    let w = Array.unsafe_get aux_ar !i in
-    let (accu, v') = f !r w v in
-    r := accu;
-    if v == v' then incr i
-    else begin
-      break := false;
-      temp := Some v';
-    end
-  done;
-  if !i < len then begin
-    let ans : 'a array = Array.copy ar in
-    let v = match !temp with None -> assert false | Some x -> x in
-    Array.unsafe_set ans !i v;
-    incr i;
-    while !i < len do
-      let v = Array.unsafe_get ar !i in
-      let w = Array.unsafe_get aux_ar !i in
-      let (accu, v') = f !r w v in
-      r := accu;
-      if v != v' then Array.unsafe_set ans !i v';
-      incr i
-    done;
-    !r, ans
-  end else !r, ar
-
 let map2 f v1 v2 =
   let len1 = Array.length v1 in
   let len2 = Array.length v2 in
@@ -580,29 +451,53 @@ let rev_to_list a =
 let filter_with filter v =
   Array.of_list (CList.filter_with filter (Array.to_list v))
 
-module Fun1 =
+module Smart =
 struct
 
-  let map f arg v = match v with
-  | [| |] -> [| |]
-  | _ ->
-    let len = Array.length v in
-    let x0 = Array.unsafe_get v 0 in
-    let ans = Array.make len (f arg x0) in
-    for i = 1 to pred len do
-      let x = Array.unsafe_get v i in
-      Array.unsafe_set ans i (f arg x)
+  (* If none of the elements is changed by f we return ar itself.
+     The while loop looks for the first such an element.
+     If found, we break here and the new array is produced,
+     but f is not re-applied to elements that are already checked *)
+  let map f (ar : 'a array) =
+    let len = Array.length ar in
+    let i = ref 0 in
+    let break = ref true in
+    let temp = ref None in
+    while !break && (!i < len) do
+      let v = Array.unsafe_get ar !i in
+      let v' = f v in
+      if v == v' then incr i
+      else begin
+        break := false;
+        temp := Some v';
+      end
     done;
-    ans
+    if !i < len then begin
+      (** The array is not the same as the original one *)
+      let ans : 'a array = Array.copy ar in
+      let v = match !temp with None -> assert false | Some x -> x in
+      Array.unsafe_set ans !i v;
+      incr i;
+      while !i < len do
+        let v = Array.unsafe_get ans !i in
+        let v' = f v in
+        if v != v' then Array.unsafe_set ans !i v';
+        incr i
+      done;
+      ans
+    end else ar
 
-  let smartmap f arg (ar : 'a array) =
+  let map2 f aux_ar ar =
     let len = Array.length ar in
+    let aux_len = Array.length aux_ar in
+    let () = if not (Int.equal len aux_len) then invalid_arg "Array.Smart.map2" in
     let i = ref 0 in
     let break = ref true in
     let temp = ref None in
     while !break && (!i < len) do
       let v = Array.unsafe_get ar !i in
-      let v' = f arg v in
+      let w = Array.unsafe_get aux_ar !i in
+      let v' = f w v in
       if v == v' then incr i
       else begin
         break := false;
@@ -617,13 +512,105 @@ struct
       incr i;
       while !i < len do
         let v = Array.unsafe_get ans !i in
-        let v' = f arg v in
+        let w = Array.unsafe_get aux_ar !i in
+        let v' = f w v in
         if v != v' then Array.unsafe_set ans !i v';
         incr i
       done;
       ans
     end else ar
 
+  (** Same as [Smart.map] but threads a state meanwhile *)
+  let fold_left_map f accu (ar : 'a array) =
+    let len = Array.length ar in
+    let i = ref 0 in
+    let break = ref true in
+    let r = ref accu in
+    (** This variable is never accessed unset *)
+    let temp = ref None in
+    while !break && (!i < len) do
+      let v = Array.unsafe_get ar !i in
+      let (accu, v') = f !r v in
+      r := accu;
+      if v == v' then incr i
+      else begin
+        break := false;
+        temp := Some v';
+      end
+    done;
+    if !i < len then begin
+      let ans : 'a array = Array.copy ar in
+      let v = match !temp with None -> assert false | Some x -> x in
+      Array.unsafe_set ans !i v;
+      incr i;
+      while !i < len do
+        let v = Array.unsafe_get ar !i in
+        let (accu, v') = f !r v in
+        r := accu;
+        if v != v' then Array.unsafe_set ans !i v';
+        incr i
+      done;
+      !r, ans
+    end else !r, ar
+
+  (** Same as [Smart.map2] but threads a state meanwhile *)
+  let fold_left2_map f accu aux_ar ar =
+    let len = Array.length ar in
+    let aux_len = Array.length aux_ar in
+    let () = if not (Int.equal len aux_len) then invalid_arg "Array.Smart.fold_left2_map" in
+    let i = ref 0 in
+    let break = ref true in
+    let r = ref accu in
+    (** This variable is never accessed unset *)
+    let temp = ref None in
+    while !break && (!i < len) do
+      let v = Array.unsafe_get ar !i in
+      let w = Array.unsafe_get aux_ar !i in
+      let (accu, v') = f !r w v in
+      r := accu;
+      if v == v' then incr i
+      else begin
+        break := false;
+        temp := Some v';
+      end
+    done;
+    if !i < len then begin
+      let ans : 'a array = Array.copy ar in
+      let v = match !temp with None -> assert false | Some x -> x in
+      Array.unsafe_set ans !i v;
+      incr i;
+      while !i < len do
+        let v = Array.unsafe_get ar !i in
+        let w = Array.unsafe_get aux_ar !i in
+        let (accu, v') = f !r w v in
+        r := accu;
+        if v != v' then Array.unsafe_set ans !i v';
+        incr i
+      done;
+      !r, ans
+    end else !r, ar
+
+end
+
+(* Deprecated aliases *)
+let smartmap = Smart.map
+let smartfoldmap = Smart.fold_left_map
+
+module Fun1 =
+struct
+
+  let map f arg v = match v with
+  | [| |] -> [| |]
+  | _ ->
+    let len = Array.length v in
+    let x0 = Array.unsafe_get v 0 in
+    let ans = Array.make len (f arg x0) in
+    for i = 1 to pred len do
+      let x = Array.unsafe_get v i in
+      Array.unsafe_set ans i (f arg x)
+    done;
+    ans
+
   let iter f arg v =
     let len = Array.length v in
     for i = 0 to pred len do
@@ -641,4 +628,40 @@ struct
       f arg x1 x2
     done
 
+  module Smart =
+  struct
+
+    let map f arg (ar : 'a array) =
+      let len = Array.length ar in
+      let i = ref 0 in
+      let break = ref true in
+      let temp = ref None in
+      while !break && (!i < len) do
+        let v = Array.unsafe_get ar !i in
+        let v' = f arg v in
+        if v == v' then incr i
+        else begin
+          break := false;
+          temp := Some v';
+        end
+      done;
+      if !i < len then begin
+        (** The array is not the same as the original one *)
+        let ans : 'a array = Array.copy ar in
+        let v = match !temp with None -> assert false | Some x -> x in
+        Array.unsafe_set ans !i v;
+        incr i;
+        while !i < len do
+          let v = Array.unsafe_get ans !i in
+          let v' = f arg v in
+          if v != v' then Array.unsafe_set ans !i v';
+          incr i
+        done;
+        ans
+      end else ar
+
+  end
+
+  let smartmap = Smart.map
+
 end
diff --git a/clib/cArray.mli b/clib/cArray.mli
index c461d856b..d800e79ed 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -83,24 +83,14 @@ sig
       Raise [Failure "Array.chop"] if [i] is not a valid index. *)
 
   val smartmap : ('a -> 'a) -> 'a array -> 'a array
-  (** [smartmap f a] behaves as [map f a] but returns [a] instead of a copy when
-      [f x == x] for all [x] in [a]. *)
-
-  val smartmap2 : ('a -> 'b -> 'b) -> 'a array -> 'b array -> 'b array
-  (** [smartmap2 f a b] behaves as [map2 f a b] but returns [a] instead of a copy when
-      [f x y == y] for all [x] in [a] and [y] in [b] pointwise. *)
+  [@@ocaml.deprecated "Same as [Smart.map]"]
 
   val smartfoldmap : ('r -> 'a -> 'r * 'a) -> 'r -> 'a array -> 'r * 'a array
-  (** [smartfoldmap f a b] behaves as [fold_left_map] but
-      returns [b] as second component instead of a copy of [b] when
-      the output array is pointwise the same as the input array [b] *)
-
-  val smartfoldmap2 : ('r -> 'a -> 'b -> 'r * 'b) -> 'r -> 'a array -> 'b array -> 'r * 'b array
-  (** [smartfoldmap2 f a b c] behaves as [fold_left2_map] but
-      returns [c] as second component instead of a copy of [c] when
-      the output array is pointwise the same as the input array [c] *)
+  [@@ocaml.deprecated "Same as [Smart.fold_left_map]"]
 
   val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
+  (** See also [Smart.map2] *)
+
   val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map3 :
     ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
@@ -113,13 +103,13 @@ sig
 
   val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
   (** [fold_left_map f e_0 [|l_1...l_n|] = e_n,[|k_1...k_n|]]
-    where [(e_i,k_i)=f e_{i-1} l_i] *)
+    where [(e_i,k_i)=f e_{i-1} l_i]; see also [Smart.fold_left_map] *)
 
   val fold_right_map : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
   (** Same, folding on the right *)
 
   val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array
-  (** Same with two arrays, folding on the left *)
+  (** Same with two arrays, folding on the left; see also [Smart.fold_left2_map] *)
 
   val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
   (** Same with two arrays, folding on the left *)
@@ -148,6 +138,31 @@ sig
   (** [filter_with b a] selects elements of [a] whose corresponding element in
       [b] is [true].  Raise [Invalid_argument _] when sizes differ. *)
 
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a array -> 'a array
+    (** [Smart.map f a] behaves as [map f a] but returns [a] instead of a copy when
+        [f x == x] for all [x] in [a]. *)
+
+    val map2 : ('a -> 'b -> 'b) -> 'a array -> 'b array -> 'b array
+    (** [Smart.map2 f a b] behaves as [map2 f a b] but returns [a] instead of a copy when
+        [f x y == y] for all [x] in [a] and [y] in [b] pointwise. *)
+
+    val fold_left_map : ('a -> 'b -> 'a * 'b) -> 'a -> 'b array -> 'a * 'b array
+    (** [Smart.fold_left_mapf a b] behaves as [fold_left_map] but
+        returns [b] as second component instead of a copy of [b] when
+        the output array is pointwise the same as the input array [b] *)
+
+    val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'c) -> 'a -> 'b array -> 'c array -> 'a * 'c array
+    (** [Smart.fold_left2_map f a b c] behaves as [fold_left2_map] but
+        returns [c] as second component instead of a copy of [c] when
+        the output array is pointwise the same as the input array [c] *)
+
+  end
+  (** The functions defined in this module are optimized specializations
+      of the main ones, when the returned array is of same type as one of
+      the original array. *)
+
 end
 
 include ExtS
@@ -158,7 +173,7 @@ sig
   (** [Fun1.map f x v = map (f x) v] *)
 
   val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
-  (** [Fun1.smartmap f x v = smartmap (f x) v] *)
+  [@@ocaml.deprecated "Same as [Fun1.Smart.map]"]
 
   val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit
   (** [Fun1.iter f x v = iter (f x) v] *)
@@ -166,6 +181,12 @@ sig
   val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit
   (** [Fun1.iter2 f x v1 v2 = iter (f x) v1 v2] *)
 
+  module Smart :
+  sig
+    val map : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
+    (** [Fun1.Smart.map f x v = Smart.map (f x) v] *)
+  end
+
 end
 (** The functions defined in this module are the same as the main ones, except
     that they are all higher-order, and their function arguments have an
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 2ab545612..f14122ca1 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -285,7 +285,7 @@ let map sigma f c = match kind sigma c with
       else mkLetIn (na, b', t', k')
   | App (b,l) ->
       let b' = f b in
-      let l' = Array.smartmap f l in
+      let l' = Array.Smart.map f l in
       if b'==b && l'==l then c
       else mkApp (b', l')
   | Proj (p,t) ->
@@ -293,23 +293,23 @@ let map sigma f c = match kind sigma c with
       if t' == t then c
       else mkProj (p, t')
   | Evar (e,l) ->
-      let l' = Array.smartmap f l in
+      let l' = Array.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
   | Case (ci,p,b,bl) ->
       let b' = f b in
       let p' = f p in
-      let bl' = Array.smartmap f bl in
+      let bl' = Array.Smart.map f bl in
       if b'==b && p'==p && bl'==bl then c
       else mkCase (ci, p', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
 
@@ -339,7 +339,7 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
     else mkLetIn (na, b', t', c')
   | App (c, al) ->
     let c' = f l c in
-    let al' = CArray.Fun1.smartmap f l al in
+    let al' = CArray.Fun1.Smart.map f l al in
     if c' == c && al' == al then c0
     else mkApp (c', al')
   | Proj (p, t) ->
@@ -347,25 +347,25 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
     if t' == t then c0
     else mkProj (p, t')
   | Evar (e, al) ->
-    let al' = CArray.Fun1.smartmap f l al in
+    let al' = CArray.Fun1.Smart.map f l al in
     if al' == al then c0
     else mkEvar (e, al')
   | Case (ci, p, c, bl) ->
     let p' = f l p in
     let c' = f l c in
-    let bl' = CArray.Fun1.smartmap f l bl in
+    let bl' = CArray.Fun1.Smart.map f l bl in
     if p' == p && c' == c && bl' == bl then c0
     else mkCase (ci, p', c', bl')
   | Fix (ln, (lna, tl, bl)) ->
-    let tl' = CArray.Fun1.smartmap f l tl in
+    let tl' = CArray.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
+    let bl' = CArray.Fun1.Smart.map f l' bl in
     if tl' == tl && bl' == bl then c0
     else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-    let tl' = CArray.Fun1.smartmap f l tl in
+    let tl' = CArray.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
+    let bl' = CArray.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
 let iter sigma f c = match kind sigma c with
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b806dce0b..dc6a103e0 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -610,12 +610,12 @@ let rec subst_notation_constr subst bound raw =
 
   | NRec (fk,idl,dll,tl,bl) ->
       let dll' =
-	Array.smartmap (List.smartmap (fun (na,oc,b as x) ->
-	  let oc' =  Option.smartmap (subst_notation_constr subst bound) oc in
+        Array.Smart.map (List.smartmap (fun (na,oc,b as x) ->
+          let oc' =  Option.smartmap (subst_notation_constr subst bound) oc in
 	  let b' =  subst_notation_constr subst bound b in
 	  if oc' == oc && b' == b then x else (na,oc',b'))) dll in
-      let tl' = Array.smartmap (subst_notation_constr subst bound) tl in
-      let bl' = Array.smartmap (subst_notation_constr subst bound) bl in
+      let tl' = Array.Smart.map (subst_notation_constr subst bound) tl in
+      let bl' = Array.Smart.map (subst_notation_constr subst bound) bl in
       if dll' == dll && tl' == tl && bl' == bl then raw else
 	  NRec (fk,idl,dll',tl',bl')
 
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 641d424e2..0727eaeac 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -152,7 +152,7 @@ let rec map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam
   | Levar (evk, args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Levar (evk, args')
   | Lprod(dom,codom) ->
     let dom' = f n dom in
@@ -167,19 +167,19 @@ let rec map_lam_with_binders g f n lam =
     if body == body' && def == def' then lam else Llet(id,def',body')
   | Lapp(fct,args) ->
     let fct' = f n fct in
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if fct == fct' && args == args' then lam else mkLapp fct' args'
   | Lcase(ci,rtbl,t,a,branches) ->
     let const = branches.constant_branches in
     let nonconst = branches.nonconstant_branches in
     let t' = f n t in
     let a' = f n a in
-    let const' = Array.smartmap (f n) const in
+    let const' = Array.Smart.map (f n) const in
     let on_b b =
       let (ids,body) = b in
       let body' = f (g (Array.length ids) n) body in
       if body == body' then b else (ids,body') in
-    let nonconst' = Array.smartmap on_b nonconst in
+    let nonconst' = Array.Smart.map on_b nonconst in
     let branches' =
       if const == const' && nonconst == nonconst' then
         branches
@@ -190,20 +190,20 @@ let rec map_lam_with_binders g f n lam =
     if t == t' && a == a' && branches == branches' then lam else
       Lcase(ci,rtbl,t',a',branches')
   | Lfix(init,(ids,ltypes,lbodies)) ->
-    let ltypes' = Array.smartmap (f n) ltypes in
-    let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+    let ltypes' = Array.Smart.map (f n) ltypes in
+    let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
     if ltypes == ltypes' && lbodies == lbodies' then lam
     else Lfix(init,(ids,ltypes',lbodies'))
   | Lcofix(init,(ids,ltypes,lbodies)) ->
-    let ltypes' = Array.smartmap (f n) ltypes in
-    let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+    let ltypes' = Array.Smart.map (f n) ltypes in
+    let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
     if ltypes == ltypes' && lbodies == lbodies' then lam
     else Lcofix(init,(ids,ltypes',lbodies'))
   | Lmakeblock(tag,args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Lmakeblock(tag,args')
   | Lprim(kn,ar,op,args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Lprim(kn,ar,op,args')
   | Lproj(i,kn,arg) ->
     let arg' = f n arg in
@@ -216,7 +216,7 @@ and map_uint g f n u =
   match u with
   | UintVal _ -> u
   | UintDigits(args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then u else UintDigits(args')
   | UintDecomp(a) ->
     let a' = f n a in
@@ -250,7 +250,7 @@ let rec lam_exsubst subst lam =
 
 let lam_subst_args subst args =
   if is_subs_id subst then args
-  else Array.smartmap (lam_exsubst subst) args
+  else Array.Smart.map (lam_exsubst subst) args
 
 (** Simplification of lambda expression *)
 
@@ -316,7 +316,7 @@ and simplify_app substf f substa args =
     simplify_app substf f subst_id args
   | _ -> mkLapp (simplify substf f) (simplify_args substa args)
 
-and simplify_args subst args = Array.smartmap (simplify subst) args
+and simplify_args subst args = Array.Smart.map (simplify subst) args
 
 and reduce_lapp substf lids body substa largs =
   match lids, largs with
diff --git a/kernel/constr.ml b/kernel/constr.ml
index bc486210d..a1779b36d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -509,7 +509,7 @@ let map f c = match kind c with
       else mkLetIn (na, b', t', k')
   | App (b,l) ->
       let b' = f b in
-      let l' = Array.smartmap f l in
+      let l' = Array.Smart.map f l in
       if b'==b && l'==l then c
       else mkApp (b', l')
   | Proj (p,t) ->
@@ -517,23 +517,23 @@ let map f c = match kind c with
       if t' == t then c
       else mkProj (p, t')
   | Evar (e,l) ->
-      let l' = Array.smartmap f l in
+      let l' = Array.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
   | Case (ci,p,b,bl) ->
       let b' = f b in
       let p' = f p in
-      let bl' = Array.smartmap f bl in
+      let bl' = Array.Smart.map f bl in
       if b'==b && p'==p && bl'==bl then c
       else mkCase (ci, p', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
 
@@ -565,7 +565,7 @@ let fold_map f accu c = match kind c with
       else accu, mkLetIn (na, b', t', k')
   | App (b,l) ->
       let accu, b' = f accu b in
-      let accu, l' = Array.smartfoldmap f accu l in
+      let accu, l' = Array.Smart.fold_left_map f accu l in
       if b'==b && l'==l then accu, c
       else accu, mkApp (b', l')
   | Proj (p,t) ->
@@ -573,23 +573,23 @@ let fold_map f accu c = match kind c with
       if t' == t then accu, c
       else accu, mkProj (p, t')
   | Evar (e,l) ->
-      let accu, l' = Array.smartfoldmap f accu l in
+      let accu, l' = Array.Smart.fold_left_map f accu l in
       if l'==l then accu, c
       else accu, mkEvar (e, l')
   | Case (ci,p,b,bl) ->
       let accu, b' = f accu b in
       let accu, p' = f accu p in
-      let accu, bl' = Array.smartfoldmap f accu bl in
+      let accu, bl' = Array.Smart.fold_left_map f accu bl in
       if b'==b && p'==p && bl'==bl then accu, c
       else accu, mkCase (ci, p', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
-      let accu, tl' = Array.smartfoldmap f accu tl in
-      let accu, bl' = Array.smartfoldmap f accu bl in
+      let accu, tl' = Array.Smart.fold_left_map f accu tl in
+      let accu, bl' = Array.Smart.fold_left_map f accu bl in
       if tl'==tl && bl'==bl then accu, c
       else accu, mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-      let accu, tl' = Array.smartfoldmap f accu tl in
-      let accu, bl' = Array.smartfoldmap f accu bl in
+      let accu, tl' = Array.Smart.fold_left_map f accu tl in
+      let accu, bl' = Array.Smart.fold_left_map f accu bl in
       if tl'==tl && bl'==bl then accu, c
       else accu, mkCoFix (ln,(lna,tl',bl'))
 
@@ -625,7 +625,7 @@ let map_with_binders g f l c0 = match kind c0 with
     else mkLetIn (na, b', t', c')
   | App (c, al) ->
     let c' = f l c in
-    let al' = CArray.Fun1.smartmap f l al in
+    let al' = CArray.Fun1.Smart.map f l al in
     if c' == c && al' == al then c0
     else mkApp (c', al')
   | Proj (p, t) ->
@@ -633,25 +633,25 @@ let map_with_binders g f l c0 = match kind c0 with
     if t' == t then c0
     else mkProj (p, t')
   | Evar (e, al) ->
-    let al' = CArray.Fun1.smartmap f l al in
+    let al' = CArray.Fun1.Smart.map f l al in
     if al' == al then c0
     else mkEvar (e, al')
   | Case (ci, p, c, bl) ->
     let p' = f l p in
     let c' = f l c in
-    let bl' = CArray.Fun1.smartmap f l bl in
+    let bl' = CArray.Fun1.Smart.map f l bl in
     if p' == p && c' == c && bl' == bl then c0
     else mkCase (ci, p', c', bl')
   | Fix (ln, (lna, tl, bl)) ->
-    let tl' = CArray.Fun1.smartmap f l tl in
+    let tl' = CArray.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
+    let bl' = CArray.Fun1.Smart.map f l' bl in
     if tl' == tl && bl' == bl then c0
     else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-    let tl' = CArray.Fun1.smartmap f l tl in
+    let tl' = CArray.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
+    let bl' = CArray.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
 type instance_compare_fn = GlobRef.t -> int ->
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 }
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 9c2fa0546..0027ebecf 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -367,7 +367,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
@@ -396,21 +396,21 @@ let rec map_kn f f' c =
 	    else mkLetIn (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 mkApp (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 mkEvar (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 mkFix (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 mkCoFix (ln,(lna,tl',bl'))
       | _ -> c
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 01ddffe3e..12cd5fe83 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -102,10 +102,10 @@ let rec map_lam_with_binders g f n lam =
       if body == body' && def == def' then lam else Llet(id,def',body')
   | Lapp(fct,args) ->
       let fct' = f n fct in
-      let args' = Array.smartmap (f n) args in
+      let args' = Array.Smart.map (f n) args in
       if fct == fct' && args == args' then lam else mkLapp fct' args'
   | Lprim(prefix,kn,op,args) ->
-      let args' = Array.smartmap (f n) args in
+      let args' = Array.Smart.map (f n) args in
       if args == args' then lam else Lprim(prefix,kn,op,args')
   | Lcase(annot,t,a,br) ->
       let t' = f n t in
@@ -116,7 +116,7 @@ let rec map_lam_with_binders g f n lam =
 	  if Array.is_empty ids then f n body 
 	  else f (g (Array.length ids) n) body in
 	if body == body' then b else (cn,ids,body') in
-      let br' = Array.smartmap on_b br in
+      let br' = Array.Smart.map on_b br in
       if t == t' && a == a' && br == br' then lam else Lcase(annot,t',a',br')
   | Lif(t,bt,bf) ->
       let t' = f n t in
@@ -124,17 +124,17 @@ let rec map_lam_with_binders g f n lam =
       let bf' = f n bf in
       if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf')
   | Lfix(init,(ids,ltypes,lbodies)) ->
-      let ltypes' = Array.smartmap (f n) ltypes in
-      let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+      let ltypes' = Array.Smart.map (f n) ltypes in
+      let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
       if ltypes == ltypes' && lbodies == lbodies' then lam
       else Lfix(init,(ids,ltypes',lbodies'))
   | Lcofix(init,(ids,ltypes,lbodies)) ->
-      let ltypes' = Array.smartmap (f n) ltypes in
-      let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+      let ltypes' = Array.Smart.map (f n) ltypes in
+      let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
       if ltypes == ltypes' && lbodies == lbodies' then lam
       else Lcofix(init,(ids,ltypes',lbodies'))
   | Lmakeblock(prefix,cn,tag,args) ->
-      let args' = Array.smartmap (f n) args in
+      let args' = Array.Smart.map (f n) args in
       if args == args' then lam else Lmakeblock(prefix,cn,tag,args')
   | Luint u ->
     let u' = map_uint g f n u in
@@ -144,7 +144,7 @@ and map_uint g f n u =
   match u with
   | UintVal _ -> u
   | UintDigits(prefix,c,args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then u else UintDigits(prefix,c,args')
   | UintDecomp(prefix,c,a) ->
     let a' = f n a in
@@ -177,7 +177,7 @@ let rec lam_exsubst subst lam =
 
 let lam_subst_args subst args =
   if is_subs_id subst then args 
-  else Array.smartmap (lam_exsubst subst) args
+  else Array.Smart.map (lam_exsubst subst) args
   
 (** Simplification of lambda expression *)
       
@@ -272,7 +272,7 @@ and simplify_app substf f substa args =
   (* TODO | Lproj -> simplify if the argument is known or a known global *)
   | _ -> mkLapp (simplify substf f) (simplify_args substa args)
   
-and simplify_args subst args = Array.smartmap (simplify subst) args
+and simplify_args subst args = Array.Smart.map (simplify subst) args
 
 and reduce_lapp substf lids body substa largs =
   match lids, largs with
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8e19fa4e5..6bcffdd45 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -853,7 +853,7 @@ struct
   let length a = Array.length a
 
   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 of_array t'
 
   let levels x = LSet.of_array x
@@ -890,7 +890,7 @@ 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
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 0e371025e..d2ba6af7b 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -103,11 +103,11 @@ let rec map f t = match t with
 let smartmap f t = match t with
     Param _ -> t
   | Node (a,sons) ->
-      let a'=f a and sons' = Array.smartmap (map f) sons in
+      let a'=f a and sons' = Array.Smart.map (map f) sons in
       if a'==a && sons'==sons then t
       else Node (a',sons')
   | Rec(j,defs) ->
-      let defs' = Array.smartmap (map f) defs in
+      let defs' = Array.Smart.map (map f) defs in
       if defs'==defs then t
       else Rec(j,defs')
 
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 8e53a044d..4c6156a38 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -457,7 +457,7 @@ let rec canonize_name sigma c =
       | LetIn (na,b,t,ct) ->
 	  mkLetIn (na, func b,func t,func ct)
       | App (ct,l) ->
-	  mkApp (func ct,Array.smartmap func l)
+          mkApp (func ct,Array.Smart.map func l)
       | Proj(p,c) ->
 	let p' = Projection.map (fun kn ->
           Constant.make1 (Constant.canonical kn)) p in 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 0901acc7d..f508a8860 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -541,12 +541,12 @@ let dump_unused_vars a =
 
     | MLcase (t,e,br) ->
        let e' = ren env e in
-       let br' = Array.smartmap (ren_branch env) br in
+       let br' = Array.Smart.map (ren_branch env) br in
        if e' == e && br' == br then a else MLcase (t,e',br')
 
     | MLfix (i,ids,v) ->
        let env' = List.init (Array.length ids) (fun _ -> ref false) @ env in
-       let v' = Array.smartmap (ren env') v in
+       let v' = Array.Smart.map (ren env') v in
        if v' == v then a else MLfix (i,ids,v')
 
     | MLapp (b,l) ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 56e582891..ea2889dea 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 3ae04cd4f..95f02dceb 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 ccfb7f990..bc7ed6137 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 34d7a0798..e07ed7711 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'))
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 4934afa83..218b2671e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -481,7 +481,7 @@ and mk_arggoals sigma goal goalacc funty allargs =
       let env = Goal.V82.env sigma goal in
       raise (RefinerError (env,sigma,CannotApply (t, harg)))
   in
-  Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs
+  Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs
 
 and mk_casegoals sigma goal goalacc p c =
   let env = Goal.V82.env sigma goal in
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 6d0da0dfa..21520f5d2 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -53,7 +53,7 @@ let subst_one_scheme subst (ind,const) =
   (subst_ind subst ind,subst_constant subst const)
 
 let subst_scheme (subst,(kind,l)) =
-  (kind,Array.map (subst_one_scheme subst) l)
+  (kind,Array.Smart.map (subst_one_scheme subst) l)
 
 let discharge_scheme (_,(kind,l)) =
   Some (kind,Array.map (fun (ind,const) ->
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 2a41a50dd..3de7fe06b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -400,9 +400,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
        lb_type_of_p >>= fun (lb_type_of_p,eff) ->
        Proofview.tclEVARMAP >>= fun sigma ->
        let lb_args = Array.append (Array.append
-                          (Array.map (fun x -> x) v)
-                          (Array.map (fun x -> do_arg sigma x 1) v))
-                          (Array.map (fun x -> do_arg sigma x 2) v)
+                          v
+                          (Array.Smart.map (fun x -> do_arg sigma x 1) v))
+                          (Array.Smart.map (fun x -> do_arg sigma x 2) v)
         in let app =  if Array.is_empty lb_args
                        then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
            in
@@ -471,9 +471,9 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
 		 user_err err_msg
                in let bl_args =
                         Array.append (Array.append
-                          (Array.map (fun x -> x) v)
-                          (Array.map (fun x -> do_arg sigma x 1) v))
-                          (Array.map (fun x -> do_arg sigma x 2) v )
+                          v
+                          (Array.Smart.map (fun x -> do_arg sigma x 1) v))
+                          (Array.Smart.map (fun x -> do_arg sigma x 2) v )
                 in
                 let app =  if Array.is_empty bl_args
                            then bl_t1 else mkApp (bl_t1,bl_args)
@@ -923,7 +923,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 	    (* left *)
 	    Tacticals.New.tclTHENLIST [
 	      simplest_left;
-              apply (EConstr.of_constr (mkApp(blI,Array.map(fun x->mkVar x) xargs)));
+              apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs)));
               Auto.default_auto
             ]
             ;
@@ -939,7 +939,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
               assert_by (Name freshH3)
 		(EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])))
 		(Tacticals.New.tclTHENLIST [
-		  apply (EConstr.of_constr (mkApp(lbI,Array.map (fun x->mkVar x) xargs)));
+                  apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs)));
                   Auto.default_auto
 		]);
 	      Equality.general_rewrite_bindings_in true
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 *)