5 files changed, 11 insertions, 11 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 6b14fd304..23c1028a4 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -216,7 +216,7 @@ let rec type_v_knsubst s = function
 and type_c_knsubst s ((id,v),e,pl,q) =
   ((id, type_v_knsubst s v), e, 
    List.map (fun p -> { p with p_value = subst_mps s p.p_value }) pl,
-   option_map (fun q -> { q with a_value = subst_mps s q.a_value }) q)
+   Option.map (fun q -> { q with a_value = subst_mps s q.a_value }) q)
 
 and binder_knsubst s (id,b) = 
   (id, match b with BindType v -> BindType (type_v_knsubst s v) | _ -> b)
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index 1a4ddbc2c..a341ba2ba 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -76,9 +76,9 @@ let rec abstract_post ren env (e,q) =
   let after_id id = id_of_string ((string_of_id id) ^ "'") in
   let (_,go) = Peffect.get_repr e in
   let al = List.map (fun id -> (id,after_id id)) go in
-  let q = option_map (named_app (subst_in_constr al)) q in
+  let q = Option.map (named_app (subst_in_constr al)) q in
   let tgo = List.map (fun (id,aid) -> (aid, trad_type_in_env ren env id)) al in
-  option_map (named_app (abstract tgo)) q
+  Option.map (named_app (abstract tgo)) q
 
 (* Translation of effects types in cic types.
  *
@@ -365,7 +365,7 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
 	    @(eq_phi ren'' env s svi tf)
 	    @(List.map (fun c -> CC_hole c) holes))
   in
-  let qapp' = option_map (named_app (subst_in_constr svi)) qapp in
+  let qapp' = Option.map (named_app (subst_in_constr svi)) qapp in
   let t = 
     make_let_in ren'' env fe [] (current_vars ren''' outf,qapp')
       (res,tyres) (t,ty)
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 72b609b24..bb9a355c3 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -787,7 +787,7 @@ END
 
 VERNAC COMMAND EXTEND Correctness
   [ "Correctness" preident(str) program(pgm) then_tac(tac) ]
-   -> [ Ptactic.correctness str pgm (option_map Tacinterp.interp tac) ]
+   -> [ Ptactic.correctness str pgm (Option.map Tacinterp.interp tac) ]
 END
 
 (* Show Programs *)
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 46cd12403..e4bac65f4 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -41,7 +41,7 @@ let anonymous x = { a_name = Anonymous; a_value = x }
 let anonymous_pre b x = { p_assert = b; p_name = Anonymous; p_value = x }
 
 let force_name f x =
-  option_map (fun q -> { a_name = Name (f q.a_name); a_value = q.a_value }) x
+  Option.map (fun q -> { a_name = Name (f q.a_name); a_value = q.a_value }) x
 
 let force_post_name x = force_name post_name x
 
@@ -143,7 +143,7 @@ let rec type_c_subst s ((id,t),e,p,q) =
   let s' = s @ List.map (fun (x,x') -> (at_id x "", at_id x' "")) s in
   (id, type_v_subst s t), Peffect.subst s e,
   List.map (pre_app (subst_in_constr s)) p,
-  option_map (post_app (subst_in_constr s')) q
+  Option.map (post_app (subst_in_constr s')) q
 
 and type_v_subst s = function
     Ref v -> Ref (type_v_subst s v)
@@ -160,7 +160,7 @@ and binder_subst s = function
 let rec type_c_rsubst s ((id,t),e,p,q) =
   (id, type_v_rsubst s t), e,
     List.map (pre_app (real_subst_in_constr s)) p,
-    option_map (post_app (real_subst_in_constr s)) q
+    Option.map (post_app (real_subst_in_constr s)) q
 
 and type_v_rsubst s = function
     Ref v -> Ref (type_v_rsubst s v)
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index 70e9eee29..258a46150 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -64,7 +64,7 @@ let update_post env top ef c =
 let force_post up env top q e =
   let (res,ef,p,_) = e.info.kappa in
   let q' = 
-    if up then option_map (named_app (update_post env top ef)) q else q 
+    if up then Option.map (named_app (update_post env top ef)) q else q 
   in
   let i = { env = e.info.env; kappa = (res,ef,p,q') } in
   { desc = e.desc; pre = e.pre; post = q'; loc = e.loc; info = i }
@@ -260,7 +260,7 @@ and propagate ren p =
     | Apply (f,l) ->
 	let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in
 	if ok then
-	  let q = option_map (named_app (real_subst_in_constr so)) qapp in
+	  let q = Option.map (named_app (real_subst_in_constr so)) qapp in
 	  post_if_none env q p
 	else
 	  p
@@ -285,7 +285,7 @@ and propagate ren p =
 	    None -> Some (anonymous s)
 	  | Some i -> Some { a_value = conj i.a_value s; a_name = i.a_name }
 	in
-	let q = option_map (named_app abstract_unit) q in
+	let q = Option.map (named_app abstract_unit) q in
 	post_if_none env q p
 
     | SApp ([Variable id], [e1;e2])