Moving Option.smart_map to Option.Smart.map.

5 files changed, 15 insertions, 15 deletions

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;