From b81fafbb8fbcba0cd54ea93fd44e6bd69540324a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 5 Apr 2018 11:33:30 +0200
Subject: CArray: adding combinators.

---
 clib/cArray.ml  | 82 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 clib/cArray.mli | 10 +++++++
 2 files changed, 92 insertions(+)

diff --git a/clib/cArray.ml b/clib/cArray.ml
index 071f4689b..c1013dff4 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -50,7 +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
   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
   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 :
@@ -359,6 +361,39 @@ let smartmap f (ar : 'a array) =
     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
@@ -392,6 +427,43 @@ let smartfoldmap f accu (ar : 'a array) =
     !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
@@ -559,4 +631,14 @@ struct
       f arg x
     done
 
+  let iter2 f arg v1 v2 =
+    let len1 = Array.length v1 in
+    let len2 = Array.length v2 in
+    let () = if not (Int.equal len2 len1) then invalid_arg "Array.Fun1.iter2" in
+    for i = 0 to pred len1 do
+      let x1 = uget v1 i in
+      let x2 = uget v2 i in
+      f arg x1 x2
+    done
+
 end
diff --git a/clib/cArray.mli b/clib/cArray.mli
index 9c2f521f4..56cc3656d 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -86,9 +86,16 @@ sig
   (** [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. *)
+
   val smartfoldmap : ('r -> 'a -> 'r * 'a) -> 'r -> 'a array -> 'r * 'a array
   (** Same as [smartmap] but threads an additional state left-to-right. *)
 
+  val smartfoldmap2 : ('r -> 'a -> 'b -> 'r * 'b) -> 'r -> 'a array -> 'b array -> 'r * 'b array
+  (** Same as [smartmap2] but threads an additional state left-to-right. *)
+
   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 :
@@ -152,6 +159,9 @@ sig
   val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit
   (** [Fun1.iter f x v = iter (f x) v] *)
 
+  val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit
+  (** [Fun1.iter2 f x v1 v2 = iter (f x) v1 v2] *)
+
 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
-- 
cgit v1.2.3


From 4e207da568b31fb3fd097fb584f4722bd7166fcf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 29 Apr 2018 21:51:05 +0200
Subject: Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their
 documentation.

This follows the model of smartmap and smartmap2.
---
 clib/cArray.mli | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/clib/cArray.mli b/clib/cArray.mli
index 56cc3656d..c461d856b 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -91,10 +91,14 @@ sig
       [f x y == y] for all [x] in [a] and [y] in [b] pointwise. *)
 
   val smartfoldmap : ('r -> 'a -> 'r * 'a) -> 'r -> 'a array -> 'r * 'a array
-  (** Same as [smartmap] but threads an additional state left-to-right. *)
+  (** [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
-  (** Same as [smartmap2] but threads an additional state left-to-right. *)
+  (** [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] *)
 
   val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
-- 
cgit v1.2.3


From f2ab2825077bf8344d2e55be433efb1891212589 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 May 2018 13:34:22 +0200
Subject: Collecting Array.smart_* functions into a module Array.Smart.

---
 checker/declarations.ml      |  20 +--
 checker/univ.ml              |   6 +-
 clib/cArray.ml               | 327 +++++++++++++++++++++++--------------------
 clib/cArray.mli              |  55 +++++---
 engine/eConstr.ml            |  28 ++--
 interp/notation_ops.ml       |   8 +-
 kernel/clambda.ml            |  26 ++--
 kernel/constr.ml             |  42 +++---
 kernel/declareops.ml         |  18 +--
 kernel/mod_subst.ml          |  14 +-
 kernel/nativelambda.ml       |  22 +--
 kernel/univ.ml               |   4 +-
 lib/rtree.ml                 |   4 +-
 plugins/cc/ccalgo.ml         |   2 +-
 plugins/extraction/mlutil.ml |   4 +-
 pretyping/detyping.ml        |   6 +-
 pretyping/glob_ops.ml        |   2 +-
 pretyping/patternops.ml      |  10 +-
 pretyping/reductionops.ml    |   4 +-
 proofs/logic.ml              |   2 +-
 tactics/ind_tables.ml        |   2 +-
 vernac/auto_ind_decl.ml      |  16 +--
 vernac/himsg.ml              |   2 +-
 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 *)
 
-- 
cgit v1.2.3


From 944f62d08b7d78bcb20dd12ba138891d432b5987 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 13 May 2018 15:21:10 +0200
Subject: Exporting Fun1 within Array so that Array.Fun1 and not only
 CArray.Fun1 works.

---
 clib/cArray.ml            | 12 ++++++++++++
 clib/cArray.mli           | 42 +++++++++++++++++++++---------------------
 engine/eConstr.ml         | 20 ++++++++++----------
 engine/termops.ml         |  2 +-
 kernel/cClosure.ml        | 32 ++++++++++++++++----------------
 kernel/constr.ml          | 28 ++++++++++++++--------------
 kernel/esubst.ml          |  2 +-
 kernel/reduction.ml       |  2 +-
 pretyping/reductionops.ml |  4 ++--
 9 files changed, 78 insertions(+), 66 deletions(-)

diff --git a/clib/cArray.ml b/clib/cArray.ml
index 6ea46655f..b26dae729 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -81,6 +81,18 @@ sig
     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
+  module Fun1 :
+  sig
+    val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array
+    val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
+    [@@ocaml.deprecated "Same as [Fun1.Smart.map]"]
+    val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit
+    val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit
+    module Smart :
+    sig
+      val map : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
+    end
+  end
 end
 
 include Array
diff --git a/clib/cArray.mli b/clib/cArray.mli
index d800e79ed..8bf33f82f 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -163,32 +163,32 @@ sig
       of the main ones, when the returned array is of same type as one of
       the original array. *)
 
-end
-
-include ExtS
+  module Fun1 :
+  sig
+    val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array
+    (** [Fun1.map f x v = map (f x) v] *)
 
-module Fun1 :
-sig
-  val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array
-  (** [Fun1.map f x v = map (f x) v] *)
+    val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
+    [@@ocaml.deprecated "Same as [Fun1.Smart.map]"]
 
-  val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
-  [@@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] *)
 
-  val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit
-  (** [Fun1.iter f x v = iter (f x) v] *)
+    val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit
+    (** [Fun1.iter2 f x v1 v2 = iter (f x) v1 v2] *)
 
-  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
 
-  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
+  (** 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
+      additional parameter. This allows us to prevent closure creation in critical
+      cases. *)
 
 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
-    additional parameter. This allows us to prevent closure creation in critical
-    cases. *)
+
+include ExtS
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index f14122ca1..f1530b2d1 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -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.Smart.map f l al in
+    let al' = Array.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.Smart.map f l al in
+    let al' = Array.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.Smart.map f l bl in
+    let bl' = Array.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.Smart.map f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.Smart.map f l' bl in
+    let bl' = Array.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.Smart.map f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.Smart.map f l' bl in
+    let bl' = Array.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
 let iter sigma f c = match kind sigma c with
@@ -391,9 +391,9 @@ let iter_with_full_binders sigma g f n c =
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
-  | App (c,l) -> f n c; CArray.Fun1.iter f n l
-  | Evar (_,l) -> CArray.Fun1.iter f n l
-  | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+  | App (c,l) -> f n c; Array.Fun1.iter f n l
+  | Evar (_,l) -> Array.Fun1.iter f n l
+  | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
diff --git a/engine/termops.ml b/engine/termops.ml
index c271d9d99..053fcc3db 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -931,7 +931,7 @@ let dependent_main noevar sigma m t =
       match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
 	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
-	    CArray.Fun1.iter deprec m
+            Array.Fun1.iter deprec m
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
 	| _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 08114abc4..435cf0a79 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -482,7 +482,7 @@ let rec lft_fconstr n ft =
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
-  if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v
+  if Int.equal k 0 then v else Array.Fun1.map lft_fconstr k v
 
 let clos_rel e i =
   match expand_rel i e with
@@ -547,7 +547,7 @@ let mk_clos_vect env v = match v with
 | [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|]
 | [|v0; v1; v2; v3|] ->
   [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|]
-| v -> CArray.Fun1.map mk_clos env v
+| v -> Array.Fun1.map mk_clos env v
 
 (* Translate the head constructor of t from constr to fconstr. This
    function is parameterized by the function to apply on the direct
@@ -562,7 +562,7 @@ let mk_clos_deep clos_fun env t =
           term = FCast (clos_fun env a, k, clos_fun env b)}
     | App (f,v) ->
         { norm = Red;
-	  term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) }
+          term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) }
     | Proj (p,c) ->
 	{ norm = Red;
 	  term = FProj (p, clos_fun env c) }
@@ -605,21 +605,21 @@ let rec to_constr constr_fun lfts v =
 		Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve)
     | FFix ((op,(lna,tys,bds)),e) ->
         let n = Array.length bds in
-        let ftys = CArray.Fun1.map mk_clos e tys in
-        let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
+        let ftys = Array.Fun1.map mk_clos e tys in
+        let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
 	let lfts' = el_liftn n lfts in
-	mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
-		         CArray.Fun1.map constr_fun lfts' fbds))
+        mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
+                         Array.Fun1.map constr_fun lfts' fbds))
     | FCoFix ((op,(lna,tys,bds)),e) ->
         let n = Array.length bds in
-        let ftys = CArray.Fun1.map mk_clos e tys in
-        let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
+        let ftys = Array.Fun1.map mk_clos e tys in
+        let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
 	let lfts' = el_liftn (Array.length bds) lfts in
-	mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
-		           CArray.Fun1.map constr_fun lfts' fbds))
+        mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
+                           Array.Fun1.map constr_fun lfts' fbds))
     | FApp (f,ve) ->
 	mkApp (constr_fun lfts f,
-	       CArray.Fun1.map constr_fun lfts ve)
+               Array.Fun1.map constr_fun lfts ve)
     | FProj (p,c) ->
         mkProj (p,constr_fun lfts c)
 
@@ -1024,14 +1024,14 @@ and norm_head info tab m =
       | FProd(na,dom,rng) ->
           mkProd(na, kl info tab dom, kl info tab rng)
       | FCoFix((n,(na,tys,bds)),e) ->
-          let ftys = CArray.Fun1.map mk_clos e tys in
+          let ftys = Array.Fun1.map mk_clos e tys in
           let fbds =
-            CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+            Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
           mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FFix((n,(na,tys,bds)),e) ->
-          let ftys = CArray.Fun1.map mk_clos e tys in
+          let ftys = Array.Fun1.map mk_clos e tys in
           let fbds =
-            CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+            Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
           mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FEvar((i,args),env) ->
           mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index a1779b36d..8f83d6baa 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -468,16 +468,16 @@ let iter_with_binders g f n c = match kind c with
   | Prod (_,t,c) -> f n t; f (g n) c
   | Lambda (_,t,c) -> f n t; f (g n) c
   | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
-  | App (c,l) -> f n c; CArray.Fun1.iter f n l
-  | Evar (_,l) -> CArray.Fun1.iter f n l
-  | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+  | App (c,l) -> f n c; Array.Fun1.iter f n l
+  | Evar (_,l) -> Array.Fun1.iter f n l
+  | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(_,tl,bl)) ->
-      CArray.Fun1.iter f n tl;
-      CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
+      Array.Fun1.iter f n tl;
+      Array.Fun1.iter f (iterate g (Array.length tl) n) bl
   | CoFix (_,(_,tl,bl)) ->
-      CArray.Fun1.iter f n tl;
-      CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
+      Array.Fun1.iter f n tl;
+      Array.Fun1.iter f (iterate g (Array.length tl) n) bl
 
 (* [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -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.Smart.map f l al in
+    let al' = Array.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.Smart.map f l al in
+    let al' = Array.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.Smart.map f l bl in
+    let bl' = Array.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.Smart.map f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.Smart.map f l' bl in
+    let bl' = Array.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.Smart.map f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.Smart.map f l' bl in
+    let bl' = Array.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
 type instance_compare_fn = GlobRef.t -> int ->
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 91cc64523..4b8edf63f 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -140,7 +140,7 @@ let rec comp mk_cl s1 s2 =
     | ESID _, _ -> s2
     | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
     | _, CONS(x,s') ->
-        CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
+        CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
     | CONS(x,s), SHIFT(k,s') ->
         let lg = Array.length x in
         if k == lg then comp mk_cl s s'
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 81fbd4f5e..38106fbf6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -84,7 +84,7 @@ let map_lift (l : lift) (v : fconstr array) = match v with
 | [|c0; c1|] -> [|(l, c0); (l, c1)|]
 | [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|]
 | [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|]
-| v -> CArray.Fun1.map (fun l t -> (l, t)) l v
+| v -> Array.Fun1.map (fun l t -> (l, t)) l v
 
 let pure_stack lfts stk =
   let rec pure_rec lfts stk =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e07ed7711..6fde86837 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.Smart.map 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.Smart.map 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'))
-- 
cgit v1.2.3


From 33b5074f24270c202a9922f21d445c12cc6b3b3d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 May 2018 13:34:46 +0200
Subject: Collecting List.smart_* functions into a module List.Smart.

---
 checker/declarations.ml      |  2 +-
 checker/term.ml              |  2 +-
 checker/univ.ml              |  6 +++---
 clib/cList.ml                | 48 +++++++++++++++++++++++++++++---------------
 clib/cList.mli               | 17 ++++++++++++----
 interp/impargs.ml            |  2 +-
 interp/notation.ml           |  2 +-
 interp/notation_ops.ml       | 12 +++++------
 kernel/context.ml            |  4 ++--
 kernel/declareops.ml         |  8 ++++----
 kernel/modops.ml             |  4 ++--
 kernel/univ.ml               | 10 ++++-----
 library/lib.ml               |  2 +-
 plugins/extraction/mlutil.ml |  6 +++---
 pretyping/detyping.ml        | 12 +++++------
 pretyping/glob_ops.ml        | 10 ++++-----
 pretyping/patternops.ml      |  4 ++--
 pretyping/pretyping.ml       |  2 +-
 pretyping/recordops.ml       |  2 +-
 pretyping/typeclasses.ml     | 10 ++++-----
 proofs/redexpr.ml            |  4 ++--
 tactics/hints.ml             | 12 +++++------
 22 files changed, 103 insertions(+), 78 deletions(-)

diff --git a/checker/declarations.ml b/checker/declarations.ml
index ca31e143f..3368d68f7 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -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
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 d3eab8613..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
 
@@ -956,7 +956,7 @@ let subst_instance_instance s 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'
 
diff --git a/clib/cList.ml b/clib/cList.ml
index 8727f4696..7621793d4 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -39,6 +39,7 @@ sig
   val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
   val filter_with : bool list -> 'a list -> 'a list
   val smartmap : ('a -> 'a) -> 'a list -> 'a list
+  [@@ocaml.deprecated "Same as [Smart.map]"]
   val map_left : ('a -> 'b) -> 'a list -> 'b list
   val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
   val map2_i :
@@ -53,6 +54,7 @@ sig
     (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
   val map_of_array : ('a -> 'b) -> 'a array -> 'b list
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
+  [@@ocaml.deprecated "Same as [Smart.map]"]
   val extend : bool list -> 'a -> 'a list -> 'a list
   val count : ('a -> bool) -> 'a list -> int
   val index : 'a eq -> 'a -> 'a list -> int
@@ -117,6 +119,12 @@ sig
     ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
   val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
 
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a list -> 'a list
+    val filter : ('a -> bool) -> 'a list -> 'a list
+  end
+
   module type MonoS = sig
     type elt
     val equal : elt list -> elt list -> bool
@@ -365,13 +373,6 @@ let assign l n e =
   in
   assrec [] l n
 
-let rec smartmap f l = match l with
-    [] -> l
-  | h::tl ->
-      let h' = f h and tl' = smartmap f tl in
-        if h'==h && tl'==tl then l
-        else h'::tl'
-
 let map_left = map
 
 let map2_i f i l1 l2 =
@@ -398,15 +399,6 @@ let map4 f l1 l2 l3 l4 =
   in
   map (l1,l2,l3,l4)
 
-let rec smartfilter f l = match l with
-    [] -> l
-  | h::tl ->
-      let tl' = smartfilter f tl in
-        if f h then
-          if tl' == tl then l
-          else h :: tl'
-        else tl'
-
 let rec extend l a l' = match l,l' with
   | true::l, b::l' -> b :: extend l a l'
   | false::l, l' -> a :: extend l a l'
@@ -896,6 +888,30 @@ let rec factorize_left cmp = function
       (a,(b::List.map snd al)) :: factorize_left cmp l'
   | [] -> []
 
+module Smart =
+struct
+
+  let rec map f l = match l with
+    [] -> l
+  | h::tl ->
+      let h' = f h and tl' = map f tl in
+        if h'==h && tl'==tl then l
+        else h'::tl'
+
+  let rec filter f l = match l with
+    [] -> l
+  | h::tl ->
+      let tl' = filter f tl in
+        if f h then
+          if tl' == tl then l
+          else h :: tl'
+        else tl'
+
+end
+
+let smartmap = Smart.map
+let smartfilter = Smart.filter
+
 module type MonoS = sig
   type elt
   val equal : elt list -> elt list -> bool
diff --git a/clib/cList.mli b/clib/cList.mli
index fd6d6a158..b3c151098 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -75,8 +75,7 @@ sig
       [b] is [true]. Raise [Invalid_argument _] when sizes differ. *)
 
   val smartmap : ('a -> 'a) -> 'a list -> 'a list
-  (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
-    [f ai == ai], then [smartmap f l == l] *)
+  [@@ocaml.deprecated "Same as [Smart.map]"]
 
   val map_left : ('a -> 'b) -> 'a list -> 'b list
   (** As [map] but ensures the left-to-right order of evaluation. *)
@@ -97,8 +96,7 @@ sig
   (** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *)
 
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
-  (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
-    [f ai = true], then [smartfilter f l == l] *)
+  [@@ocaml.deprecated "Same as [Smart.filter]"]
 
   val extend : bool list -> 'a -> 'a list -> 'a list
 (** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n];
@@ -258,6 +256,17 @@ sig
 
   val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
 
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a list -> 'a list
+    (** [Smart.map f [a1...an] = List.map f [a1...an]] but if for all i
+        [f ai == ai], then [Smart.map f l == l] *)
+
+    val filter : ('a -> bool) -> 'a list -> 'a list
+    (** [Smart.filter f [a1...an] = List.filter f [a1...an]] but if for all i
+        [f ai = true], then [Smart.filter f l == l] *)
+  end
+
   module type MonoS = sig
     type elt
     val equal : elt list -> elt list -> bool
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 7e4c4ef4f..2db67c299 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -538,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) =
   let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
 
 let subst_implicits (subst,(req,l)) =
-  (ImplLocal,List.smartmap (subst_implicits_decl subst) l)
+  (ImplLocal,List.Smart.map (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
   let map (decl, impl) = match impl with
diff --git a/interp/notation.ml b/interp/notation.ml
index e6df7b96c..192c477be 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -741,7 +741,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
         match subst_scope_class subst cl with
         | Some cl'  as ocl' when cl' != cl -> ocl'
         | _ -> ocl in
-  let cls' = List.smartmap subst_cl cls in
+  let cls' = List.Smart.map subst_cl cls in
   (ArgsScopeNoDischarge,r',n,scl,cls')
 
 let discharge_arguments_scope (_,(req,r,n,l,_)) =
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index dc6a103e0..eeda607e6 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -521,7 +521,7 @@ let rec subst_pat subst pat =
   | PatVar _ -> pat
   | PatCstr (((kn,i),j),cpl,n) ->
       let kn' = subst_mind subst kn
-      and cpl' = List.smartmap (subst_pat subst) cpl in
+      and cpl' = List.Smart.map (subst_pat subst) cpl in
       if kn' == kn && cpl' == cpl then pat else
         DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n)
 
@@ -536,7 +536,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NApp (r,rl) ->
       let r' = subst_notation_constr subst bound r
-      and rl' = List.smartmap (subst_notation_constr subst bound) rl in
+      and rl' = List.Smart.map (subst_notation_constr subst bound) rl in
 	if r' == r && rl' == rl then raw else
 	  NApp(r',rl')
 
@@ -573,7 +573,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NCases (sty,rtntypopt,rl,branches) ->
       let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt
-      and rl' = List.smartmap
+      and rl' = List.Smart.map
         (fun (a,(n,signopt) as x) ->
 	  let a' = subst_notation_constr subst bound a in
 	  let signopt' = Option.map (fun ((indkn,i),nal as z) ->
@@ -581,9 +581,9 @@ let rec subst_notation_constr subst bound raw =
 	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
         rl
-      and branches' = List.smartmap
+      and branches' = List.Smart.map
                         (fun (cpl,r as branch) ->
-                           let cpl' = List.smartmap (subst_pat subst) cpl
+                           let cpl' = List.Smart.map (subst_pat subst) cpl
                            and r' = subst_notation_constr subst bound r in
                              if cpl' == cpl && r' == r then branch else
                                (cpl',r'))
@@ -610,7 +610,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NRec (fk,idl,dll,tl,bl) ->
       let dll' =
-        Array.Smart.map (List.smartmap (fun (na,oc,b as x) ->
+        Array.Smart.map (List.Smart.map (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
diff --git a/kernel/context.ml b/kernel/context.ml
index 4f3f649c1..5d4a10184 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -192,7 +192,7 @@ struct
   let equal eq l = List.equal (fun c -> Declaration.equal eq c) l
 
   (** Map all terms in a given rel-context. *)
-  let map f = List.smartmap (Declaration.map_constr f)
+  let map f = List.Smart.map (Declaration.map_constr f)
 
   (** Perform a given action on every declaration in a given rel-context. *)
   let iter f = List.iter (Declaration.iter_constr f)
@@ -392,7 +392,7 @@ struct
   let equal eq l = List.equal (fun c -> Declaration.equal eq c) l
 
   (** Map all terms in a given named-context. *)
-  let map f = List.smartmap (Declaration.map_constr f)
+  let map f = List.Smart.map (Declaration.map_constr f)
 
   (** Perform a given action on every declaration in a given named-context. *)
   let iter f = List.iter (Declaration.iter_constr f)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 90a6eb6f7..f2f43144e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -42,7 +42,7 @@ let map_decl_arity f g = function
 
 let hcons_template_arity ar =
   { template_param_levels = ar.template_param_levels;
-      (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *)
+      (* List.Smart.map (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *)
     template_level = Univ.hcons_univ ar.template_level }
 
 (** {6 Constants } *)
@@ -70,7 +70,7 @@ let is_opaque cb = match cb.const_body with
 let subst_rel_declaration sub =
   RelDecl.map_constr (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 subst_const_type sub arity =
   if is_empty_subst sub then arity
@@ -117,7 +117,7 @@ let subst_const_body sub cb =
 let hcons_rel_decl =
   RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Constr.hcons %> RelDecl.map_type Constr.hcons
 
-let hcons_rel_context l = List.smartmap hcons_rel_decl l
+let hcons_rel_context l = List.Smart.map hcons_rel_decl l
 
 let hcons_const_def = function
   | Undef inl -> Undef inl
@@ -331,7 +331,7 @@ and hcons_structure_body sb =
     let sfb' = hcons_structure_field_body sfb in
     if l == l' && sfb == sfb' then fb else (l', sfb')
   in
-  List.smartmap map sb
+  List.Smart.map map sb
 
 and hcons_module_signature ms =
   hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms
diff --git a/kernel/modops.ml b/kernel/modops.ml
index bbf160db2..daee0f187 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -197,7 +197,7 @@ let rec subst_structure sub do_delta sign =
       let mtb' = subst_modtype sub do_delta mtb in
       if mtb==mtb' then orig else (l,SFBmodtype mtb')
   in
-  List.smartmap subst_body sign
+  List.Smart.map subst_body sign
 
 and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body =
   fun is_mod sub subst_impl do_delta mb ->
@@ -595,7 +595,7 @@ and clean_field l field = match field with
     if mb==mb' then field else (lab,SFBmodule mb')
   |_ -> field
 
-and clean_structure l = List.smartmap (clean_field l)
+and clean_structure l = List.Smart.map (clean_field l)
 
 and clean_signature l =
   functor_smartmap (clean_module_type l) (clean_structure l)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6bcffdd45..9782312ca 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -456,10 +456,10 @@ struct
   let super l = 
     if is_small l then type1
     else
-      List.smartmap (fun x -> Expr.successor x) l
+      List.Smart.map (fun x -> Expr.successor x) l
 
   let addn n l =
-    List.smartmap (fun x -> Expr.addn n x) l
+    List.Smart.map (fun x -> Expr.addn n x) l
 
   let rec merge_univs l1 l2 =
     match l1, l2 with
@@ -500,7 +500,7 @@ struct
 
   let for_all = List.for_all
 
-  let smartmap = List.smartmap
+  let smart_map = List.Smart.map
 
   let map = List.map
 end
@@ -894,7 +894,7 @@ let subst_instance_instance s 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'
 
@@ -1100,7 +1100,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'
 
diff --git a/library/lib.ml b/library/lib.ml
index 8a54995b9..128b27e75 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -51,7 +51,7 @@ let subst_objects subst seg =
       if obj' == obj then node else
 	(id, obj')
   in
-    List.smartmap subst_one seg
+    List.Smart.map subst_one seg
 
 (*let load_and_subst_objects i prefix subst seg =
   List.rev (List.fold_left (fun seg (id,obj as node) ->
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index f508a8860..9f5c1f1a1 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -550,15 +550,15 @@ let dump_unused_vars a =
        if v' == v then a else MLfix (i,ids,v')
 
     | MLapp (b,l) ->
-       let b' = ren env b and l' = List.smartmap (ren env) l in
+       let b' = ren env b and l' = List.Smart.map (ren env) l in
        if b' == b && l' == l then a else MLapp (b',l')
 
     | MLcons(t,r,l) ->
-       let l' = List.smartmap (ren env) l in
+       let l' = List.Smart.map (ren env) l in
        if l' == l then a else MLcons (t,r,l')
 
     | MLtuple l ->
-       let l' = List.smartmap (ren env) l in
+       let l' = List.Smart.map (ren env) l in
        if l' == l then a else MLtuple l'
 
     | MLmagic b ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ea2889dea..e306fd6b3 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')
 
@@ -964,7 +964,7 @@ let rec subst_glob_constr subst = DAst.map (function
   | 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) ->
+      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
@@ -972,10 +972,10 @@ let rec subst_glob_constr subst = DAst.map (function
             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')))
@@ -1003,7 +1003,7 @@ let rec subst_glob_constr subst = DAst.map (function
       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) ->
+        (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
           if ty'==ty && obd'==obd then dcl else (na,k,obd',ty')))
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 95f02dceb..102e89400 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -338,7 +338,7 @@ let bound_glob_vars =
    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)
 
@@ -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 bc7ed6137..b425dc0e2 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -297,7 +297,7 @@ let rec subst_pattern subst pat =
 	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) ->
@@ -334,7 +334,7 @@ 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')
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6bf852fcd..de72f9427 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 84aceeedd..334bfc895 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -69,7 +69,7 @@ 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
+   List.Smart.map
      (Option.smartmap (fun kn -> fst (subst_con_kn subst kn)))
     projs
   in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 11cc6c1f0..5ad9dc691 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -180,11 +180,11 @@ 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.smartmap do_subst_gr) grs,
     do_subst_ctx ctx in
-  let do_subst_projs projs = List.smartmap (fun (x, y, z) -> 
+  let do_subst_projs projs = List.Smart.map (fun (x, y, z) ->
     (x, y, Option.smartmap do_subst_con z)) projs in
   { cl_univs = cl.cl_univs;
     cl_impl = do_subst_gr cl.cl_impl;
@@ -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.smartmap 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
@@ -239,7 +239,7 @@ let discharge_class (_,cl) =
         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
       }
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 6fb411938..a75711bae 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -92,9 +92,9 @@ let cache_strategy (_,str) =
 
 let subst_strategy (subs,(local,obj)) =
   local,
-  List.smartmap
+  List.Smart.map
     (fun (k,ql as entry) ->
-      let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in
+      let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in
       if ql==ql' then entry else (k,ql'))
     obj
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 39034a19b..4eaff3fb9 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -448,7 +448,7 @@ let subst_path_atom subst p =
   | PathAny -> p
   | PathHints grs ->
     let gr' gr = fst (subst_global subst gr) in
-    let grs' = List.smartmap gr' grs in
+    let grs' = List.Smart.map gr' grs in
       if grs' == grs then p else PathHints grs'
 
 let rec subst_hints_path subst hp =
@@ -654,7 +654,7 @@ struct
 
   let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l
 
-  let remove_sdl p sdl = List.smartfilter p sdl 
+  let remove_sdl p sdl = List.Smart.filter p sdl
 
   let remove_he st p se =
     let sl1' = remove_sdl p se.sentry_nopat in
@@ -666,7 +666,7 @@ struct
     let filter (_, h) =
       match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
     let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
-    let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
+    let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
 
   let remove_one gr db = remove_list [gr] db
@@ -1104,13 +1104,13 @@ let subst_autohint (subst, obj) =
   let action = match obj.hint_action with
     | CreateDB _ -> obj.hint_action
     | AddTransparency (grs, b) ->
-      let grs' = List.smartmap (subst_evaluable_reference subst) grs in
+      let grs' = List.Smart.map (subst_evaluable_reference subst) grs in
       if grs == grs' then obj.hint_action else AddTransparency (grs', b)
     | AddHints hintlist ->
-      let hintlist' = List.smartmap subst_hint hintlist in
+      let hintlist' = List.Smart.map subst_hint hintlist in
       if hintlist' == hintlist then obj.hint_action else AddHints hintlist'
     | RemoveHints grs ->
-      let grs' = List.smartmap (subst_global_reference subst) grs in
+      let grs' = List.Smart.map (subst_global_reference subst) grs in
       if grs == grs' then obj.hint_action else RemoveHints grs'
     | AddCut path ->
       let path' = subst_hints_path subst path in
-- 
cgit v1.2.3


From bb2d7f94ba8688f57dc62ca72a857b82368aa784 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 May 2018 18:23:28 +0200
Subject: Moving Option.smart_map to Option.Smart.map.

---
 checker/declarations.ml         |  2 +-
 clib/option.ml                  | 21 +++++++++++++++------
 clib/option.mli                 | 13 +++++++++++--
 interp/notation_ops.ml          | 12 ++++++------
 kernel/declareops.ml            |  6 +++---
 kernel/modops.ml                |  2 +-
 plugins/funind/indfun_common.ml | 24 ++++++++++++------------
 pretyping/detyping.ml           | 14 +++++++-------
 pretyping/glob_ops.ml           |  2 +-
 pretyping/patternops.ml         |  4 ++--
 pretyping/recordops.ml          |  2 +-
 pretyping/typeclasses.ml        |  8 ++++----
 tactics/autorewrite.ml          |  2 +-
 tactics/hints.ml                |  4 ++--
 14 files changed, 67 insertions(+), 49 deletions(-)

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 3368d68f7..ddd505a9a 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -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/clib/option.ml b/clib/option.ml
index 32fe2fc5f..7a3d5f934 100644
--- a/clib/option.ml
+++ b/clib/option.ml
@@ -100,12 +100,6 @@ let map f = function
   | Some y -> Some (f y)
   | _ -> None
 
-(** [smartmap f x] does the same as [map f x] except that it tries to share
-    some memory. *)
-let smartmap f = function
-  | Some y as x -> let y' = f y in if y' == y then x else Some y'
-  | _ -> None
-
 (** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *)
 let fold_left f a = function
   | Some y -> f a y
@@ -176,6 +170,21 @@ let lift2 f x y =
   | _,_ -> None
 
 
+(** {6 Smart operations} *)
+
+module Smart =
+struct
+
+  (** [Smart.map f x] does the same as [map f x] except that it tries to share
+      some memory. *)
+  let map f = function
+    | Some y as x -> let y' = f y in if y' == y then x else Some y'
+    | _ -> None
+
+end
+
+let smartmap = Smart.map
+
 (** {6 Operations with Lists} *)
 
 module List =
diff --git a/clib/option.mli b/clib/option.mli
index 14fa9da38..8f82bf090 100644
--- a/clib/option.mli
+++ b/clib/option.mli
@@ -75,9 +75,8 @@ val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit
 (** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *)
 val map : ('a -> 'b) -> 'a option -> 'b option
 
-(** [smartmap f x] does the same as [map f x] except that it tries to share
-    some memory. *)
 val smartmap : ('a -> 'a) -> 'a option -> 'a option
+[@@ocaml.deprecated "Same as [Smart.map]"]
 
 (** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *)
 val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b
@@ -123,6 +122,16 @@ val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option
     [Some w]. It is [None] otherwise. *)
 val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
 
+(** {6 Smart operations} *)
+
+module Smart :
+sig
+
+  (** [Smart.map f x] does the same as [map f x] except that it tries to share
+      some memory. *)
+  val map : ('a -> 'a) -> 'a option -> 'a option
+
+end
 
 (** {6 Operations with Lists} *)
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index eeda607e6..e51c69136 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -566,13 +566,13 @@ let rec subst_notation_constr subst bound raw =
 
   | NLetIn (n,r1,t,r2) ->
       let r1' = subst_notation_constr subst bound r1 in
-      let t' = Option.smartmap (subst_notation_constr subst bound) t in
+      let t' = Option.Smart.map (subst_notation_constr subst bound) t in
       let r2' = subst_notation_constr subst bound r2 in
 	if r1' == r1 && t == t' && r2' == r2 then raw else
 	  NLetIn (n,r1',t',r2')
 
   | NCases (sty,rtntypopt,rl,branches) ->
-      let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt
+      let rtntypopt' = Option.Smart.map (subst_notation_constr subst bound) rtntypopt
       and rl' = List.Smart.map
         (fun (a,(n,signopt) as x) ->
 	  let a' = subst_notation_constr subst bound a in
@@ -594,14 +594,14 @@ let rec subst_notation_constr subst bound raw =
           NCases (sty,rtntypopt',rl',branches')
 
   | NLetTuple (nal,(na,po),b,c) ->
-      let po' = Option.smartmap (subst_notation_constr subst bound) po
+      let po' = Option.Smart.map (subst_notation_constr subst bound) po
       and b' = subst_notation_constr subst bound b
       and c' = subst_notation_constr subst bound c in
 	if po' == po && b' == b && c' == c then raw else
 	  NLetTuple (nal,(na,po'),b',c')
 
   | NIf (c,(na,po),b1,b2) ->
-      let po' = Option.smartmap (subst_notation_constr subst bound) po
+      let po' = Option.Smart.map (subst_notation_constr subst bound) po
       and b1' = subst_notation_constr subst bound b1
       and b2' = subst_notation_constr subst bound b2
       and c' = subst_notation_constr subst bound c in
@@ -611,7 +611,7 @@ let rec subst_notation_constr subst bound raw =
   | NRec (fk,idl,dll,tl,bl) ->
       let dll' =
         Array.Smart.map (List.Smart.map (fun (na,oc,b as x) ->
-          let oc' =  Option.smartmap (subst_notation_constr subst bound) oc in
+          let oc' =  Option.Smart.map (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.Smart.map (subst_notation_constr subst bound) tl in
@@ -628,7 +628,7 @@ let rec subst_notation_constr subst bound raw =
       if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
     | _ -> knd
     in
-    let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in
+    let nsolve = Option.Smart.map (Genintern.generic_substitute subst) solve in
     if nsolve == solve && nknd == knd then raw
     else NHole (nknd, naming, nsolve)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index f2f43144e..cc0b381c9 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -42,7 +42,7 @@ let map_decl_arity f g = function
 
 let hcons_template_arity ar =
   { template_param_levels = ar.template_param_levels;
-      (* List.Smart.map (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *)
+      (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
     template_level = Univ.hcons_univ ar.template_level }
 
 (** {6 Constants } *)
@@ -94,7 +94,7 @@ let subst_const_body sub cb =
   else
     let body' = subst_const_def sub cb.const_body in
     let type' = subst_const_type sub cb.const_type in
-    let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in
+    let proj' = Option.Smart.map (subst_const_proj sub) cb.const_proj in
     if body' == cb.const_body && type' == cb.const_type
       && proj' == cb.const_proj then cb
     else
@@ -217,7 +217,7 @@ let subst_mind_record sub (id, ps, pb as r) =
     else (id, ps', pb')
 
 let subst_mind_body sub mib =
-  { mind_record = Option.smartmap (Option.smartmap (subst_mind_record sub)) mib.mind_record ;
+  { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ;
     mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
     mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
diff --git a/kernel/modops.ml b/kernel/modops.ml
index daee0f187..58ebb4ad7 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -210,7 +210,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body ->
   in
   let ty' = subst_signature sub do_delta ty in
   let me' = subst_impl sub me in
-  let aty' = Option.smartmap (subst_expression sub id_delta) aty in
+  let aty' = Option.Smart.map (subst_expression sub id_delta) aty in
   let delta' = do_delta mb.mod_delta sub in
   if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta
   then mb
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 35c3acd41..b0c9ff8fc 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -269,12 +269,12 @@ let subst_Function (subst,finfos) =
   in
   let function_constant' = do_subst_con finfos.function_constant in
   let graph_ind' = do_subst_ind finfos.graph_ind in
-  let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in
-  let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in
-  let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in
-  let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in
-  let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in
-  let prop_lemma' =  Option.smartmap do_subst_con finfos.prop_lemma in
+  let equation_lemma' = Option.Smart.map do_subst_con finfos.equation_lemma in
+  let correctness_lemma' = Option.Smart.map do_subst_con finfos.correctness_lemma in
+  let completeness_lemma' = Option.Smart.map do_subst_con finfos.completeness_lemma in
+  let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in
+  let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in
+  let prop_lemma' =  Option.Smart.map do_subst_con finfos.prop_lemma in
   if function_constant' == finfos.function_constant &&
     graph_ind' == finfos.graph_ind &&
     equation_lemma' == finfos.equation_lemma &&
@@ -302,12 +302,12 @@ let classify_Function infos = Libobject.Substitute infos
 let discharge_Function (_,finfos) =
   let function_constant' = Lib.discharge_con finfos.function_constant
   and graph_ind' = Lib.discharge_inductive finfos.graph_ind
-  and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma
-  and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma
-  and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma
-  and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma
-  and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma
-  and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma
+  and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma
+  and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma
+  and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma
+  and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma
+  and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma
+  and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma
   in
   if function_constant' == finfos.function_constant &&
     graph_ind' == finfos.graph_ind &&
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e306fd6b3..779508477 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -957,17 +957,17 @@ 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
+      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
@@ -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
@@ -1005,7 +1005,7 @@ let rec subst_glob_constr subst = DAst.map (function
       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 102e89400..5056c0457 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -343,7 +343,7 @@ let map_inpattern_binders f ({loc;v=(id,nal)} as 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)
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b425dc0e2..375ed10d0 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -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
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 334bfc895..9eb410f06 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -70,7 +70,7 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
    List.Smart.map
-     (Option.smartmap (fun kn -> fst (subst_con_kn subst kn)))
+     (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/typeclasses.ml b/pretyping/typeclasses.ml
index 5ad9dc691..12a944d32 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -182,10 +182,10 @@ let subst_class (subst,cl) =
   and do_subst_gr gr = fst (subst_global subst gr) in
   let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in
   let do_subst_context (grs,ctx) =
-    List.Smart.map (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.Smart.map (fun (x, y, z) ->
-    (x, y, Option.smartmap do_subst_con z)) projs in
+    (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.Smart.map (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,7 +234,7 @@ 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;
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 627ac31f5..0b0e629ab 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -30,7 +30,7 @@ let subst_hint subst hint =
   let cst' = subst_mps subst hint.rew_lemma in
   let typ' = subst_mps subst hint.rew_type in
   let pat' = subst_mps subst hint.rew_pat in
-  let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in
+  let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in
     if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
       { hint with
 	rew_lemma = cst'; rew_type = typ';
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4eaff3fb9..3ade5314b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1065,8 +1065,8 @@ let subst_autohint (subst, obj) =
     in if gr' == gr then gr else gr'
   in
   let subst_hint (k,data as hint) =
-    let k' = Option.smartmap subst_key k in
-    let pat' = Option.smartmap (subst_pattern subst) data.pat in
+    let k' = Option.Smart.map subst_key k in
+    let pat' = Option.Smart.map (subst_pattern subst) data.pat in
     let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
     let code' = match data.code.obj with
       | Res_pf (c,t,ctx) ->
-- 
cgit v1.2.3


From d8851bbd50df1f77af0aabfe98bebd44fcb4aa02 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 May 2018 13:35:29 +0200
Subject: Moving Rtree.smart_map into Rtree.Smart.map.

---
 checker/declarations.ml |  2 +-
 kernel/declareops.ml    |  2 +-
 lib/rtree.ml            | 28 +++++++++++++++++-----------
 lib/rtree.mli           | 11 ++++++++++-
 4 files changed, 29 insertions(+), 14 deletions(-)

diff --git a/checker/declarations.ml b/checker/declarations.ml
index ddd505a9a..e1d2cf6d1 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -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
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index cc0b381c9..832d478b3 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -178,7 +178,7 @@ let recarg_length p j =
   let (_,cstrs) = Rtree.dest_node p in
   Array.length (snd (Rtree.dest_node cstrs.(j-1)))
 
-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
 
 (** {7 Substitution of inductive declarations } *)
 
diff --git a/lib/rtree.ml b/lib/rtree.ml
index d2ba6af7b..e1c6a4c4d 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -94,22 +94,28 @@ let is_node t =
       Node _ -> true
     | _ -> false
 
-
 let rec map f t = match t with
     Param(i,j) -> Param(i,j)
   | Node (a,sons) -> Node (f a, Array.map (map f) sons)
   | Rec(j,defs) -> Rec (j, Array.map (map f) defs)
 
-let smartmap f t = match t with
-    Param _ -> t
-  | Node (a,sons) ->
-      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.Smart.map (map f) defs in
-      if defs'==defs then t
-      else Rec(j,defs')
+module Smart =
+struct
+
+  let map f t = match t with
+      Param _ -> t
+    | Node (a,sons) ->
+        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.Smart.map (map f) defs in
+        if defs'==defs then t
+        else Rec(j,defs')
+
+end
+
+let smartmap = Smart.map
 
 (** Structural equality test, parametrized by an equality on elements *)
 
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 8edfc3d37..5ab14f603 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -74,13 +74,22 @@ val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -
 
 (** Iterators *)
 
+(** See also [Smart.map] *)
 val map : ('a -> 'b) -> 'a t -> 'b t
 
-(** [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
 val smartmap : ('a -> 'a) -> 'a t -> 'a t
+(** @deprecated Same as [Smart.map] *)
 
 (** A rather simple minded pretty-printer *)
 val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t
 
 val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 (** @deprecated Same as [Rtree.equal] *)
+
+module Smart :
+sig
+
+  (** [(Smart.map f t) == t] if [(f a) ==a ] for all nodes *)
+  val map : ('a -> 'a) -> 'a t -> 'a t
+
+end
-- 
cgit v1.2.3


From 153de30b639851d5ad285b765b2db7655b2cb635 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 May 2018 13:36:39 +0200
Subject: Collecting Map.smart_* functions into a module Map.Smart.

---
 clib/cMap.ml       | 58 +++++++++++++++++++++++++++++++++++++-----------------
 clib/cMap.mli      | 13 ++++++++++--
 clib/hMap.ml       | 20 +++++++++++++------
 engine/evarutil.ml |  2 +-
 engine/evd.ml      | 12 +++++------
 5 files changed, 72 insertions(+), 33 deletions(-)

diff --git a/clib/cMap.ml b/clib/cMap.ml
index 373e3f8fd..f6e52594b 100644
--- a/clib/cMap.ml
+++ b/clib/cMap.ml
@@ -35,8 +35,15 @@ sig
   val fold_left : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val smartmap : ('a -> 'a) -> 'a t -> 'a t
+  (** [@@ocaml.deprecated "Same as [Smart.map]"] *)
   val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+  (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *)
   val height : 'a t -> int
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a t -> 'a t
+    val mapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+  end
   module Unsafe :
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
@@ -59,8 +66,15 @@ sig
   val fold_left : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
   val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
   val smartmap : ('a -> 'a) -> 'a map -> 'a map
+  (** [@@ocaml.deprecated "Same as [Smart.map]"] *)
   val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
+  (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *)
   val height : 'a map -> int
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a map -> 'a map
+    val mapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
+  end
   module Unsafe :
   sig
     val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map
@@ -154,28 +168,36 @@ struct
     let accu = f k v (fold_right f r accu) in
     fold_right f l accu
 
-  let rec smartmap f (s : 'a map) = match map_prj s with
-  | MEmpty -> map_inj MEmpty
-  | MNode (l, k, v, r, h) ->
-    let l' = smartmap f l in
-    let r' = smartmap f r in
-    let v' = f v in
-    if l == l' && r == r' && v == v' then s
-    else map_inj (MNode (l', k, v', r', h))
-
-  let rec smartmapi f (s : 'a map) = match map_prj s with
-  | MEmpty -> map_inj MEmpty
-  | MNode (l, k, v, r, h) ->
-    let l' = smartmapi f l in
-    let r' = smartmapi f r in
-    let v' = f k v in
-    if l == l' && r == r' && v == v' then s
-    else map_inj (MNode (l', k, v', r', h))
-
   let height s = match map_prj s with
   | MEmpty -> 0
   | MNode (_, _, _, _, h) -> h
 
+  module Smart =
+  struct
+
+    let rec map f (s : 'a map) = match map_prj s with
+    | MEmpty -> map_inj MEmpty
+    | MNode (l, k, v, r, h) ->
+      let l' = map f l in
+      let r' = map f r in
+      let v' = f v in
+      if l == l' && r == r' && v == v' then s
+      else map_inj (MNode (l', k, v', r', h))
+
+    let rec mapi f (s : 'a map) = match map_prj s with
+    | MEmpty -> map_inj MEmpty
+    | MNode (l, k, v, r, h) ->
+      let l' = mapi f l in
+      let r' = mapi f r in
+      let v' = f k v in
+      if l == l' && r == r' && v == v' then s
+      else map_inj (MNode (l', k, v', r', h))
+
+  end
+
+  let smartmap = Smart.map
+  let smartmapi = Smart.mapi
+
   module Unsafe =
   struct
 
diff --git a/clib/cMap.mli b/clib/cMap.mli
index bb0019bb8..b45effb95 100644
--- a/clib/cMap.mli
+++ b/clib/cMap.mli
@@ -58,14 +58,23 @@ sig
   (** Folding keys in decreasing order. *)
 
   val smartmap : ('a -> 'a) -> 'a t -> 'a t
-  (** As [map] but tries to preserve sharing. *)
+  (** [@@ocaml.deprecated "Same as [Smart.map]"] *)
 
   val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
-  (** As [mapi] but tries to preserve sharing. *)
+  (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *)
 
   val height : 'a t -> int
   (** An indication of the logarithmic size of a map *)
 
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a t -> 'a t
+    (** As [map] but tries to preserve sharing. *)
+
+    val mapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+    (** As [mapi] but tries to preserve sharing. *)
+  end
+
   module Unsafe :
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 37f867c6b..b2cf47430 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -383,13 +383,21 @@ struct
     let m = Map.set k x m in
     Int.Map.set h m s
 
-  let smartmap f s =
-    let fs m = Map.smartmap f m in
-    Int.Map.smartmap fs s
+  module Smart =
+  struct
+
+    let map f s =
+      let fs m = Map.Smart.map f m in
+      Int.Map.Smart.map fs s
+
+    let mapi f s =
+      let fs m = Map.Smart.mapi f m in
+      Int.Map.Smart.map fs s
+
+  end
 
-  let smartmapi f s =
-    let fs m = Map.smartmapi f m in
-    Int.Map.smartmap fs s
+  let smartmap = Smart.map
+  let smartmapi = Smart.mapi
 
   let height s = Int.Map.height s
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index cb2d01bdf..38ceed569 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -214,7 +214,7 @@ let mk_new_meta () = EConstr.mkMeta(new_meta())
 
 let non_instantiated sigma =
   let listev = Evd.undefined_map sigma in
-  Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev
+  Evar.Map.Smart.map (fun evi -> nf_evar_info sigma evi) listev
 
 (************************)
 (* Manipulating filters *)
diff --git a/engine/evd.ml b/engine/evd.ml
index 03b843655..78d5d4c8f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -510,8 +510,8 @@ let raw_map f d =
     in
     ans
   in
-  let defn_evars = EvMap.smartmapi f d.defn_evars in
-  let undf_evars = EvMap.smartmapi f d.undf_evars in
+  let defn_evars = EvMap.Smart.mapi f d.defn_evars in
+  let undf_evars = EvMap.Smart.mapi f d.undf_evars in
   { d with defn_evars; undf_evars; }
 
 let raw_map_undefined f d =
@@ -524,7 +524,7 @@ let raw_map_undefined f d =
     in
     ans
   in
-  { d with undf_evars = EvMap.smartmapi f d.undf_evars; }
+  { d with undf_evars = EvMap.Smart.mapi f d.undf_evars; }
 
 let is_evar = mem
 
@@ -1040,11 +1040,11 @@ let map_metas_fvalue f evd =
   | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ)
   | x -> x
   in
-  set_metas evd (Metamap.smartmap map evd.metas)
+  set_metas evd (Metamap.Smart.map map evd.metas)
 
 let map_metas f evd =
   let map cl = map_clb f cl in
-  set_metas evd (Metamap.smartmap map evd.metas)
+  set_metas evd (Metamap.Smart.map map evd.metas)
 
 let meta_opt_fvalue evd mv =
   match Metamap.find mv evd.metas with
@@ -1120,7 +1120,7 @@ let retract_coercible_metas evd =
     Cltyp (na, typ)
   | v -> v
   in
-  let metas = Metamap.smartmapi map evd.metas in
+  let metas = Metamap.Smart.mapi map evd.metas in
   !mc, set_metas evd metas
 
 let evar_source_of_meta mv evd =
-- 
cgit v1.2.3


From bb189de66d46e49931206ef28c861f46bbfcb9f7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 May 2018 17:41:41 +0200
Subject: Renaming miscellaneous internal smart functions.

---
 kernel/modops.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 58ebb4ad7..203817118 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -130,10 +130,10 @@ let destr_nofunctor = function
   |NoFunctor a -> a
   |MoreFunctor _ -> error_is_a_functor ()
 
-let rec functor_smartmap fty f0 funct = match funct with
+let rec functor_smart_map fty f0 funct = match funct with
   |MoreFunctor (mbid,ty,e) ->
     let ty' = fty ty in
-    let e' = functor_smartmap fty f0 e in
+    let e' = functor_smart_map fty f0 e in
     if ty==ty' && e==e' then funct else MoreFunctor (mbid,ty',e')
   |NoFunctor a ->
     let a' = f0 a in if a==a' then funct else NoFunctor a'
@@ -245,12 +245,12 @@ and subst_expr sub do_delta seb = match seb with
     if meb==meb' && wdb==wdb' then seb else MEwith(meb',wdb')
 
 and subst_expression sub do_delta =
-  functor_smartmap
+  functor_smart_map
     (subst_modtype sub do_delta)
     (subst_expr sub do_delta)
 
 and subst_signature sub do_delta =
-  functor_smartmap
+  functor_smart_map
     (subst_modtype sub do_delta)
     (subst_structure sub do_delta)
 
@@ -598,10 +598,10 @@ and clean_field l field = match field with
 and clean_structure l = List.Smart.map (clean_field l)
 
 and clean_signature l =
-  functor_smartmap (clean_module_type l) (clean_structure l)
+  functor_smart_map (clean_module_type l) (clean_structure l)
 
 and clean_expression l =
-  functor_smartmap (clean_module_type l) (fun me -> me)
+  functor_smart_map (clean_module_type l) (fun me -> me)
 
 let rec collect_mbid l sign =  match sign with
   |MoreFunctor (mbid,ty,m) ->
-- 
cgit v1.2.3


From 5ec974962c7be7a7280a8094da733e32c232f5e0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 13 May 2018 16:06:24 +0200
Subject: Document Smart/Array changes in dev/doc/Changes.md.

---
 dev/doc/changes.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ff448abe8..774a77c8a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -28,6 +28,13 @@ Proof engine
   should indicate what the canonical form is. An important change is
   the move of `Globnames.global_reference` to `Names.GlobRef.t`.
 
+ML Libraries used by Coq
+
+- Introduction of a "Smart" module for collecting "smart*" functions, e.g.
+  Array.Smart.map.
+- Uniformization of some names, e.g. Array.Smart.fold_left_map instead
+  of Array.smartfoldmap.
+
 ### Unit testing
 
   The test suite now allows writing unit tests against OCaml code in the Coq
-- 
cgit v1.2.3