Moving Option.smart_map to Option.Smart.map.

1 files changed, 4 insertions, 4 deletions

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;