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 +++---
 2 files changed, 13 insertions(+), 13 deletions(-)

(limited to 'checker')

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
-- 
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(-)

(limited to 'checker')

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(-)

(limited to 'checker')

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(-)

(limited to 'checker')

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