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

4 files changed, 13 insertions, 13 deletions

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'