Moving Option.smart_map to Option.Smart.map.

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