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

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