Factorisation des opérations sur le type option de Util dans un module

lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting 
des fonctions (à un ou deux arguments tous ou partie de type option).

Il reste quelques opérations dans Util à propos desquelles je ne suis 
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain 
car il est tard (comme some_in qui devrait devenir Option.make je 
suppose) . Elles s'expriment souvent facilement en fonction des 
autres, par exemple "option_compare x y"  est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est 
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.

J'en ai profité aussi pour remplacer les trop nombreux "failwith" par 
des erreurs locales au module, donc plus robustes.

J'ai trouvé aussi une fonction qui était définie deux fois, et une 
définie dans un module particulier.

Mon seul bémol (mais facile à traiter) c'est la proximité entre le 
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de 
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7

27 files changed, 129 insertions, 129 deletions

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 6b14fd3048..23c1028a41 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 1a4ddbc2c7..a341ba2ba3 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 72b609b24d..bb9a355c3f 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 46cd124039..e4bac65f4b 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 70e9eee293..258a461501 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]) 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index b6367d98a2..2aca56f9bb 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -241,7 +241,7 @@ and extract_meb env mpo all = function
 and extract_module env mp all mb = 
   (* [mb.mod_expr <> None ], since we look at modules from outside. *)
   (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
-  let meb = out_some mb.mod_expr in
+  let meb = Option.get mb.mod_expr in
   let mtb = match mb.mod_user_type with None -> mb.mod_type | Some mt -> mt in
   (* Because of the "with" construct, the module type can be [MTBsig] with *)
   (* a msid different from the one of the module. Here is the patch. *)
@@ -282,7 +282,7 @@ let mono_filename f =
 	    Filename.chop_suffix f d.file_suffix 
 	  else f
 	in 
-	Some (f^d.file_suffix), option_map ((^) f) d.sig_suffix, id_of_string f
+	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f
 
 (* Builds a suitable filename from a module id *)
 
@@ -290,7 +290,7 @@ let module_filename m =
   let d = descr () in 
   let f = if d.capital_file then String.capitalize else String.uncapitalize in 
   let fn = f (string_of_id m) in
-  Some (fn^d.file_suffix), option_map ((^) fn) d.sig_suffix, m
+  Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, m
 
 (*s Extraction of one decl to stdout. *)
 
@@ -317,7 +317,7 @@ let print_structure_to_file (fn,si,mo) struc =
       else struct_ast_search (function MLmagic _ -> true | _ -> false) struc }
   in
   (* print the implementation *)
-  let cout = option_map open_out fn in 
+  let cout = Option.map open_out fn in 
   let ft = match cout with 
     | None -> !Pp_control.std_ft
     | Some cout -> Pp_control.with_output_to cout in 
@@ -330,13 +330,13 @@ let print_structure_to_file (fn,si,mo) struc =
       reset_renaming_tables OnlyLocal; 
     end; 
     msg_with ft (d.pp_struct struc);
-    option_iter close_out cout; 
+    Option.iter close_out cout; 
   with e -> 
-    option_iter close_out cout; raise e
+    Option.iter close_out cout; raise e
   end;
-  option_iter info_file fn;
+  Option.iter info_file fn;
   (* print the signature *)
-  option_iter 
+  Option.iter 
     (fun si -> 
        let cout = open_out si in
        let ft = Pp_control.with_output_to cout in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 77067b2b4c..27687ae1c3 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -310,7 +310,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
   with Not_found -> 
     (* First, if this inductive is aliased via a Module, *)
     (* we process the original inductive. *)
-    option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; 
+    Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; 
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
     let mip0 = mib.mind_packets.(0) in 
@@ -413,7 +413,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
             (Inductive.type_of_inductive env (mib,mip0))
 	  in
 	  List.iter 
-	    (option_iter 
+	    (Option.iter 
 	       (fun kn -> if Cset.mem kn !projs then add_projection n kn))
 	    (lookup_projections ip)
 	with Not_found -> ()
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 760f76c9a3..79ba0ebc5e 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -39,9 +39,9 @@ let add_structure mp msb env =
 
 let rec subst_module sub mb =
   let mtb' = Modops.subst_modtype sub mb.mod_type
-  and meb' = option_smartmap (subst_meb sub) mb.mod_expr
-  and mtb'' = option_smartmap (Modops.subst_modtype sub) mb.mod_user_type
-  and mpo' = option_smartmap (subst_mp sub) mb.mod_equiv in
+  and meb' = Option.smartmap (subst_meb sub) mb.mod_expr
+  and mtb'' = Option.smartmap (Modops.subst_modtype sub) mb.mod_user_type
+  and mpo' = Option.smartmap (subst_mp sub) mb.mod_equiv in
   if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) && 
     (mtb''==mb.mod_user_type) && (mpo'==mb.mod_equiv)
   then mb
@@ -170,7 +170,7 @@ let decl_iter_references do_term do_cons do_type =
 
 let spec_iter_references do_term do_cons do_type = function 
   | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
-  | Stype (r,_,ot) -> do_type r; option_iter (type_iter_references do_type) ot
+  | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot
   | Sval (r,t) -> do_term r; type_iter_references do_type t
 
 let struct_iter_references do_term do_cons do_type = 
@@ -241,7 +241,7 @@ let spec_type_search f = function
   | Sind (_,{ind_packets=p}) -> 
       Array.iter 
 	(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
-  | Stype (_,_,ot) -> option_iter (type_search f) ot
+  | Stype (_,_,ot) -> Option.iter (type_search f) ot
   | Sval (_,u) -> type_search f u
 
 let struct_type_search f s = 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index f3df9230d0..8ba07ab0b7 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -574,7 +574,7 @@ and pp_module_type ol = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MTsig (msid, sign) ->
       let tvm = top_visible_mp () in 
-      option_iter (fun l -> add_subst msid (MPdot (tvm, l))) ol; 
+      Option.iter (fun l -> add_subst msid (MPdot (tvm, l))) ol; 
       let mp = MPself msid in
       push_visible mp; 
       let l = map_succeed pp_specif sign in 
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index e48d47d9db..3ee1db14c9 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -98,16 +98,16 @@ let normalize_evaluables=
 
 TACTIC EXTEND firstorder
     [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> 
-      [ gen_ground_tac true (option_map eval_tactic t) (Ids l) ]
+      [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ]
 |   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> 
-      [ gen_ground_tac true (option_map eval_tactic t) (Bases l) ]
+      [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ]
 |   [ "firstorder" tactic_opt(t) ] -> 
-      [ gen_ground_tac true (option_map eval_tactic t) Void ]
+      [ gen_ground_tac true (Option.map eval_tactic t) Void ]
 END
 
 TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
-     [ gen_ground_tac false (option_map eval_tactic t) Void ]
+     [ gen_ground_tac false (Option.map eval_tactic t) Void ]
 END
 
 
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index b10aa782c8..45976d6e5b 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -882,7 +882,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let f_def = Global.lookup_constant (destConst f) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
   let f_body =
-    force (out_some f_def.const_body)
+    force (Option.get f_def.const_body)
   in
   let params,f_body_with_params = decompose_lam_n nb_params f_body in
   let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -933,8 +933,8 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
   let equation_lemma = 
     try 
       let finfos = find_Function_infos (destConst f) in 
-      mkConst (out_some finfos.equation_lemma)
-    with (Not_found | Failure "out_some" as e) -> 
+      mkConst (Option.get finfos.equation_lemma)
+    with (Not_found | Option.IsNone as e) -> 
       let f_id = id_of_label (con_label (destConst f)) in 
       (*i The next call to mk_equation_id is valid since we will construct the lemma
 	Ensures by: obvious
@@ -943,7 +943,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
       generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
       let _ =
 	match e with 
-	  | Failure "out_some" -> 
+	  | Option.IsNone -> 
 	      let finfos = find_Function_infos (destConst f) in 
 	      update_Function 
 		{finfos with
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index cb804f6f2b..72f930b0a6 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -115,7 +115,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     it_mkProd_or_LetIn 
       ~init:
       (it_mkProd_or_LetIn 
-	 ~init:(option_fold_right
+	 ~init:(Option.fold_right
 			   mkProd_or_LetIn
 			   princ_type_info.indarg
 			   princ_type_info.concl
@@ -564,9 +564,9 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
   let opacity = 
     let finfos = find_Function_infos this_block_funs.(0) in 
     try 
-      let equation =  out_some finfos.equation_lemma in  
+      let equation =  Option.get finfos.equation_lemma in  
       (Global.lookup_constant equation).Declarations.const_opaque 
-    with Failure "out_some" -> (* non recursive definition *) 
+    with Option.IsNone -> (* non recursive definition *) 
       false
   in
   let const = {const with const_entry_opaque = opacity } in 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 199e01525b..3102f1b5d7 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -48,8 +48,8 @@ let functional_induction with_clean c princl pat =
 			| InType -> finfo.rect_lemma
 		    in
 		    let princ =  (* then we get the principle *)
-		      try mkConst (out_some princ_option )
-		      with Failure "out_some" -> 
+		      try mkConst (Option.get princ_option )
+		      with Option.IsNone -> 
 			(*i If there is not default lemma defined then, 
 			  we cross our finger and try to find a lemma named f_ind 
 			  (or f_rec, f_rect) i*)
@@ -589,21 +589,21 @@ let rec add_args id new_args b =
       CApp(loc,(pf,add_args id new_args b), 
 	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
   | CCases(loc,b_option,cel,cal) -> 
-      CCases(loc,option_map (add_args id new_args) b_option,
+      CCases(loc,Option.map (add_args id new_args) b_option,
 	     List.map (fun (b,(na,b_option)) -> 
 			 add_args id new_args b,
-			 (na,option_map (add_args id new_args) b_option)) cel, 
+			 (na,Option.map (add_args id new_args) b_option)) cel, 
 	     List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
 	    )
   | CLetTuple(loc,nal,(na,b_option),b1,b2) -> 
-      CLetTuple(loc,nal,(na,option_map (add_args id new_args) b_option),
+      CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
 		add_args id new_args b1,
 		add_args id new_args b2
 	       )
 		
   | CIf(loc,b1,(na,b_option),b2,b3) -> 
       CIf(loc,add_args id new_args b1, 
-	  (na,option_map (add_args id new_args) b_option),
+	  (na,Option.map (add_args id new_args) b_option),
 	  add_args id new_args b2,
 	  add_args id new_args b3
 	 )
@@ -722,7 +722,7 @@ let make_graph (f_ref:global_reference) =
 			   )
 		       in 
 		       let rec_id = 
-			 match List.nth bl' (out_some n)  with 
+			 match List.nth bl' (Option.get n)  with 
 			   |(_,Name id) -> id | _ -> anomaly ""
 		       in
 		       let new_args = 
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 609504ba5a..c2372d3ed0 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -319,12 +319,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' = Util.option_smartmap do_subst_con finfos.equation_lemma in 
-  let correctness_lemma' = Util.option_smartmap do_subst_con finfos.correctness_lemma in 
-  let completeness_lemma' = Util.option_smartmap do_subst_con finfos.completeness_lemma in 
-  let rect_lemma' = Util.option_smartmap do_subst_con finfos.rect_lemma in
-  let rec_lemma' = Util.option_smartmap do_subst_con finfos.rec_lemma in 
-  let prop_lemma' =  Util.option_smartmap do_subst_con finfos.prop_lemma 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 
   if function_constant' == finfos.function_constant && 
     graph_ind' == finfos.graph_ind && 
     equation_lemma' == finfos.equation_lemma &&
@@ -354,12 +354,12 @@ let export_Function infos = Some 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' = Util.option_smartmap Lib.discharge_con finfos.equation_lemma 
-  and correctness_lemma' = Util.option_smartmap Lib.discharge_con finfos.correctness_lemma 
-  and completeness_lemma' = Util.option_smartmap Lib.discharge_con finfos.completeness_lemma 
-  and rect_lemma' = Util.option_smartmap Lib.discharge_con finfos.rect_lemma 
-  and rec_lemma' = Util.option_smartmap Lib.discharge_con finfos.rec_lemma
-  and prop_lemma' = Util.option_smartmap Lib.discharge_con finfos.prop_lemma
+  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
   in
   if function_constant' == finfos.function_constant && 
     graph_ind' == finfos.graph_ind && 
@@ -387,12 +387,12 @@ let pr_info f_info =
   str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
     str "function_constant_type := " ++ 
     (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
-    str "equation_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
-    str "completeness_lemma :=" ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
-    str "correctness_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
-    str "rect_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
-    str "rec_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
-    str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
+    str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
+    str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
+    str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
+    str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
+    str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
+    str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
     str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () 
 
 let pr_table tb = 
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 6171e81948..dcbefe4a40 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -665,8 +665,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       if infos.is_general ||  Rtree.is_infinite graph_def.mind_recargs
       then 
 	let eq_lemma = 
-	  try out_some (infos).equation_lemma
-	  with Failure "out_some"  -> anomaly "Cannot find equation lemma"
+	  try Option.get (infos).equation_lemma
+	  with Option.IsNone -> anomaly "Cannot find equation lemma"
 	in 
 	tclTHENSEQ[
 	  tclMAP h_intro ids;
@@ -769,7 +769,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	  Array.of_list 
 	    (List.map 
 	       (fun entry -> 
-		  (entry.Entries.const_entry_body, out_some entry.Entries.const_entry_type )
+		  (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
 	       )
 	       (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs))
 	    )
@@ -960,13 +960,13 @@ let invfun qhyp f  =
   in
   try 
     let finfos = find_Function_infos f in 
-    let f_correct = mkConst(out_some finfos.correctness_lemma) 
+    let f_correct = mkConst(Option.get finfos.correctness_lemma) 
     and kn = fst finfos.graph_ind
     in
     Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp 
   with 
     | Not_found ->  error "No graph found" 
-    | Failure "out_some"  -> error "Cannot use equivalence with graph!"
+    | Option.IsNone  -> error "Cannot use equivalence with graph!"
 
 
 let invfun qhyp f g = 
@@ -983,23 +983,23 @@ let invfun qhyp f g =
 		     try 
 		       if not (isConst f1) then failwith "";
 		       let finfos = find_Function_infos (destConst f1) in 
-		       let f_correct = mkConst(out_some finfos.correctness_lemma) 
+		       let f_correct = mkConst(Option.get finfos.correctness_lemma) 
 		       and kn = fst finfos.graph_ind
 		       in
 		       functional_inversion kn hid f1 f_correct g
-		     with | Failure "" | Failure "out_some" | Not_found -> 
+		     with | Failure "" | Option.IsNone | Not_found -> 
 		       try 
 			 let f2,_ = decompose_app args.(2) in 
 			 if not (isConst f2) then failwith "";
 			 let finfos = find_Function_infos (destConst f2) in 
-			 let f_correct = mkConst(out_some finfos.correctness_lemma) 
+			 let f_correct = mkConst(Option.get finfos.correctness_lemma) 
 			 and kn = fst finfos.graph_ind
 			 in
 			 functional_inversion kn hid  f2 f_correct g
 		       with
 			 | Failure "" -> 
 			     errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function")
-			 | Failure "out_some"  ->  
+			 | Option.IsNone  ->  
 			     if do_observe () 
 			     then
 			       error "Cannot use equivalence with graph for any side of the equality"
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index b34a1097a3..af0a2addc8 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -368,7 +368,7 @@ let raw_push_named (na,raw_value,raw_typ) env =
   match na with 
     | Anonymous -> env 
     | Name id -> 
-	let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in 
+	let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in 
 	let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in 
 	Environ.push_named (id,value,typ) env
 
@@ -398,12 +398,12 @@ let add_pat_variables pat typ env : Environ.env =
 	   | Anonymous -> assert false
 	   | Name id ->
 	       let new_t =  substl ctxt t in
-	       let new_v = option_map (substl ctxt) v in
+	       let new_v = Option.map (substl ctxt) v in
 	       observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
 			  str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
 			  str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
-			  option_fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
-			  option_fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
+			  Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
+			  Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
 		       );
 	       (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
       )
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index f9e188dacf..e8cce47adb 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -157,7 +157,7 @@ let change_vars =
 	  let new_mapping = List.fold_left remove_name_from_mapping mapping nal in 
 	  RLetTuple(loc,
 		    nal,
-		    (na, option_map (change_vars mapping) rto), 
+		    (na, Option.map (change_vars mapping) rto), 
 		    change_vars mapping b, 
 		    change_vars new_mapping e
 		   )
@@ -170,7 +170,7 @@ let change_vars =
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc,
 	      change_vars mapping b,
-	      (na,option_map (change_vars mapping) e_option),
+	      (na,Option.map (change_vars mapping) e_option),
 	      change_vars mapping lhs,
 	      change_vars mapping rhs
 	     )
@@ -338,11 +338,11 @@ let rec alpha_rt excluded rt =
 	  if idmap_is_empty mapping
 	  then rto,t,b
 	  else let replace = change_vars mapping in 
-	  (option_map replace rto, t,replace b)
+	  (Option.map replace rto, t,replace b)
 	in
 	let new_t = alpha_rt new_excluded new_t in 
 	let new_b = alpha_rt new_excluded new_b in 
-	let new_rto = option_map (alpha_rt new_excluded) new_rto  in
+	let new_rto = Option.map (alpha_rt new_excluded) new_rto  in
 	RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
     | RCases(loc,infos,el,brl) -> 
 	let new_el = 
@@ -351,7 +351,7 @@ let rec alpha_rt excluded rt =
 	RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) 
     | RIf(loc,b,(na,e_o),lhs,rhs) -> 
 	RIf(loc,alpha_rt excluded b,
-	    (na,option_map (alpha_rt excluded) e_o),
+	    (na,Option.map (alpha_rt excluded) e_o),
 	    alpha_rt excluded lhs,
 	    alpha_rt excluded rhs
 	   )
@@ -487,7 +487,7 @@ let replace_var_by_term x_id term =
       | RLetTuple(loc,nal,(na,rto),def,b) -> 
 	  RLetTuple(loc,
 		    nal,
-		    (na,option_map replace_var_by_pattern rto),
+		    (na,Option.map replace_var_by_pattern rto),
 		    replace_var_by_pattern def,
 		    replace_var_by_pattern b
 		   )
@@ -499,7 +499,7 @@ let replace_var_by_term x_id term =
 		)
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc, replace_var_by_pattern b,
-	      (na,option_map replace_var_by_pattern e_option),
+	      (na,Option.map replace_var_by_pattern e_option),
 	      replace_var_by_pattern lhs,
 	      replace_var_by_pattern rhs
 	     )
@@ -640,7 +640,7 @@ let zeta_normalize =
       | RLetTuple(loc,nal,(na,rto),def,b) -> 
 	  RLetTuple(loc,
 		    nal,
-		    (na,option_map zeta_normalize_term rto),
+		    (na,Option.map zeta_normalize_term rto),
 		    zeta_normalize_term def,
 		    zeta_normalize_term b
 		   )
@@ -652,7 +652,7 @@ let zeta_normalize =
 		)
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc, zeta_normalize_term b,
-	      (na,option_map zeta_normalize_term e_option),
+	      (na,Option.map zeta_normalize_term e_option),
 	      zeta_normalize_term lhs,
 	      zeta_normalize_term rhs
 	     )
@@ -695,17 +695,17 @@ let expand_as =
       | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
       | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
       | RLetTuple(loc,nal,(na,po),v,b) ->
-	  RLetTuple(loc,nal,(na,option_map (expand_as map) po),
+	  RLetTuple(loc,nal,(na,Option.map (expand_as map) po),
 		    expand_as map v, expand_as map b)
       | RIf(loc,e,(na,po),br1,br2) ->
-	  RIf(loc,expand_as map e,(na,option_map (expand_as map) po),
+	  RIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
       | RRec _ ->  error "Not handled RRec"
       | RDynamic _ -> error "Not handled RDynamic"
       | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
       | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
       | RCases(loc,po,el,brl) ->
-	  RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+	  RCases(loc, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
 	    
   and expand_as_br map (loc,idl,cpl,rt) = 
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 207d78b193..82fbe9c691 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -187,7 +187,7 @@ and e_my_find_search db_list local_db hdc concl =
 		 (e_trivial_fail_db db_list local_db)
 	   | Unfold_nth c -> unfold_in_concl [[],c]
 	   | Extern tacast -> Auto.conclPattern concl 
-	       (out_some p) tacast
+	       (Option.get p) tacast
        in 
        (free_try tac,fmt_autotactic t))
        (*i
@@ -400,7 +400,7 @@ and my_find_search db_list local_db hdc concl =
 		(trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> unfold_in_concl [[],c]
 	  | Extern tacast -> 
-	      conclPattern concl (out_some p) tacast))
+	      conclPattern concl (Option.get p) tacast))
     tacl
 
 and trivial_resolve db_list local_db cl = 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 150b070f88..0e4f660724 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -306,7 +306,7 @@ let make_fix_struct (n,bl) =
   let nn = List.length names in
   if nn = 1 || n = None then ctv_ID_OPT_NONE
   else 
-    let n = out_some n in 
+    let n = Option.get n in 
     if n < nn then xlate_id_opt(List.nth names n)
     else xlate_error "unexpected result of parsing for Fixpoint";;
 
@@ -429,7 +429,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
 	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
          if bl = [] then
-	   let n = out_some n in 
+	   let n = Option.get n in 
            let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
            (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
          else (make_fix_struct (n, bl),bl,arf,ardef) in
@@ -995,7 +995,7 @@ and xlate_tac =
 	  let cl_as_xlate_arg = 
 	    {cl_as_clause with 
 	       Tacexpr.onhyps = 
-		option_map 
+		Option.map 
 		  (fun l -> 
 		     List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l
 		  )
@@ -1312,7 +1312,7 @@ and coerce_genarg_to_TARG x =
 					 (snd (out_gen
 					    (rawwit_open_constr_gen b) x))))
   | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
-      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let n = Option.get (Pcoq.tactic_genarg_level s) in
       let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_COM_to_TARG t
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
@@ -1405,7 +1405,7 @@ let coerce_genarg_to_VARG x =
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
   | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
-      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let n = Option.get (Pcoq.tactic_genarg_level s) in
       let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
   | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
@@ -1857,7 +1857,7 @@ let rec xlate_vernac =
 	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
            xlate_binder_list bl, xlate_formula c))
   | VernacSuspend -> CT_suspend
-  | VernacResume idopt -> CT_resume (xlate_ident_opt (option_map snd idopt))
+  | VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt))
   | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND
 	(CT_theorem_goal
@@ -1900,7 +1900,7 @@ let rec xlate_vernac =
       (_, (add_coercion, (_,s)), binders, c1,
        rec_constructor_or_none, field_list) ->
       let record_constructor =
-        xlate_ident_opt (option_map snd rec_constructor_or_none) in
+        xlate_ident_opt (Option.map snd rec_constructor_or_none) in
       CT_record
        ((if add_coercion then CT_coercion_atm else
           CT_coerce_NONE_to_COERCION_OPT(CT_none)),
@@ -1923,7 +1923,7 @@ let rec xlate_vernac =
 	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
 	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
          if bl = [] then
-	   let n = out_some n in 
+	   let n = Option.get n in 
            let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
            (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
          else (make_fix_struct (n, bl),bl,arf,ardef) in
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index e81c9ddd5c..97dd2f143a 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -193,7 +193,7 @@ let _ =
 let subst_morph subst morph = 
   let plusm' = subst_mps subst morph.plusm in
   let multm' = subst_mps subst morph.multm in
-  let oppm' = option_smartmap (subst_mps subst) morph.oppm in
+  let oppm' = Option.smartmap (subst_mps subst) morph.oppm in
     if plusm' == morph.plusm 
       && multm' == morph.multm 
       && oppm' == morph.oppm then 
@@ -215,15 +215,15 @@ let subst_set subst cset =
     if !same then cset else cset'
 
 let subst_theory subst th = 
-  let th_equiv' = option_smartmap (subst_mps subst) th.th_equiv in
-  let th_setoid_th' = option_smartmap (subst_mps subst) th.th_setoid_th in
-  let th_morph' = option_smartmap (subst_morph subst) th.th_morph in
+  let th_equiv' = Option.smartmap (subst_mps subst) th.th_equiv in
+  let th_setoid_th' = Option.smartmap (subst_mps subst) th.th_setoid_th in
+  let th_morph' = Option.smartmap (subst_morph subst) th.th_morph in
   let th_a' = subst_mps subst th.th_a in                   
   let th_plus' = subst_mps subst th.th_plus in
   let th_mult' = subst_mps subst th.th_mult in
   let th_one' = subst_mps subst th.th_one in
   let th_zero' = subst_mps subst th.th_zero in
-  let th_opp' = option_smartmap (subst_mps subst) th.th_opp in
+  let th_opp' = Option.smartmap (subst_mps subst) th.th_opp in
   let th_eq' = subst_mps subst th.th_eq in
   let th_t' = subst_mps subst th.th_t in          
   let th_closed' = subst_set subst th.th_closed in
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 1cbae1e2ff..2c6e0ebcd4 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -451,7 +451,7 @@ let (theory_to_obj, obj_to_theory) =
 let setoid_of_relation r =
   lapp coq_mk_Setoid
     [|r.rel_a; r.rel_aeq;
-      out_some r.rel_refl; out_some r.rel_sym; out_some r.rel_trans |]
+      Option.get r.rel_refl; Option.get r.rel_sym; Option.get r.rel_trans |]
 
 let op_morph r add mul opp req m1 m2 m3 =
   lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index e54c59058f..34c398289a 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -385,7 +385,7 @@ let mkDeclTomatch na = function
 
 let map_tomatch_type f = function
   | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind)
-  | NotInd (c,t) -> NotInd (option_map f c, f t)
+  | NotInd (c,t) -> NotInd (Option.map f c, f t)
 
 let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
 let lift_tomatch_type n = liftn_tomatch_type n 1
@@ -1127,7 +1127,7 @@ let rec generalize_problem pb = function
       let tomatch = regeneralize_index_tomatch (i+1) tomatch in
       { pb with
 	  tomatch = Abstract d :: tomatch;
-          pred = option_map (generalize_predicate i d) pb'.pred }
+          pred = Option.map (generalize_predicate i d) pb'.pred }
 
 (* No more patterns: typing the right-hand-side of equations *)
 let build_leaf pb =
@@ -1142,7 +1142,7 @@ let build_leaf pb =
 let shift_problem (current,t) pb =
   {pb with
      tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
-     pred = option_map (specialize_predicate_var (current,t)) pb.pred;
+     pred = Option.map (specialize_predicate_var (current,t)) pb.pred;
      history = push_history_pattern 0 AliasLeaf pb.history;
      mat = List.map remove_current_pattern pb.mat }
 
@@ -1207,7 +1207,7 @@ let build_branch current deps pb eqns const_info =
   let cur_alias = lift (List.length sign) current in
   let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in
   let env' = push_rels sign pb.env in
-  let pred' = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
+  let pred' = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
     sign,
   { pb with
       env = env';
@@ -1279,7 +1279,7 @@ and compile_generalization pb d rest =
     { pb with
        env = push_rel d pb.env;
        tomatch = rest;
-       pred = option_map ungeneralize_predicate pb.pred;
+       pred = Option.map ungeneralize_predicate pb.pred;
        mat = List.map (push_rels_eqn [d]) pb.mat } in
   let j = compile pb in
   { uj_val = mkLambda_or_LetIn d j.uj_val;
@@ -1304,7 +1304,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
     {pb with
        env = newenv;
        tomatch = tomatch;
-       pred = option_map (lift_predicate n) pb.pred;
+       pred = Option.map (lift_predicate n) pb.pred;
        history = history;
        mat = mat } in
   let j = compile pb in
@@ -1487,7 +1487,7 @@ let extract_arity_signature env0 tomatchl tmsign =
     match tm with
       | NotInd (bo,typ) -> 
 	  (match t with
-	    | None -> [na,option_map (lift n) bo,lift n typ]
+	    | None -> [na,Option.map (lift n) bo,lift n typ]
 	    | Some (loc,_,_,_) -> 
  	    user_err_loc (loc,"",
 	    str "Unexpected type annotation for a term of non inductive type"))
@@ -1765,14 +1765,14 @@ let subst_rel_context k ctx subst =
   let (_, ctx') =
     List.fold_right 
       (fun (n, b, t) (k, acc) ->
-	 (succ k, (n, option_map (substnl subst k) b, substnl subst k t) :: acc))
+	 (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc))
       ctx (k, [])
   in ctx'
 
 let lift_rel_contextn n k sign =
   let rec liftrec k = function
     | (na,c,t)::sign ->
-	(na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
+	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
     | [] -> []
   in
   liftrec (rel_context_length sign + k) sign
@@ -2065,7 +2065,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 let liftn_rel_context n k sign =  
   let rec liftrec k = function
     | (na,c,t)::sign ->
-	(na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
+	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
     | [] -> []
   in
     liftrec (k + rel_context_length sign) sign
@@ -2074,10 +2074,10 @@ let nf_evars_env evar_defs (env : env) : env =
   let nf t = nf_isevar evar_defs t in
   let env0 : env = reset_context env in 
   let f e (na, b, t) e' : env =
-    Environ.push_named (na, option_map nf b, nf t) e'
+    Environ.push_named (na, Option.map nf b, nf t) e'
   in
   let env' = Environ.fold_named_context f ~init:env0 env in
-    Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, option_map nf b, nf t) e')
+    Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
      ~init:env' env
       
 let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 1fb079fac6..17bbb65bdc 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -305,7 +305,7 @@ module Coercion = struct
   let coerce_itf loc env isevars v t c1 =
     let evars = ref isevars in
     let coercion = coerce loc env evars t c1 in
-      !evars, option_map (app_opt coercion) v, t
+      !evars, Option.map (app_opt coercion) v, t
 	
   (* Taken from pretyping/coercion.ml *)
 
@@ -439,7 +439,7 @@ module Coercion = struct
 	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
 	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
 		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
-		    let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
+		    let v' = Option.map (whd_betadeltaiota env (evars_of isevars)) v in
 		    let (evd',b) =
 		      match v' with 
 			  Some v' ->
@@ -455,7 +455,7 @@ module Coercion = struct
 			     let env1 = push_rel (x,None,v1) env in
 			     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
 						       (Some v2) t2 u2 in
-			       (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
+			       (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2', 
 				mkProd (x, v1, t2'))
 			 | None ->
 			     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
@@ -472,7 +472,7 @@ module Coercion = struct
 			     let (evd'', v2', t2') = 
 			       let v2 =
 				 match v with 
-				     Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
+				     Some v -> Option.map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
 				   | None -> None
 			       and evd', t2 =
 				 match v1' with 
@@ -483,7 +483,7 @@ module Coercion = struct
 			       in
 				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
 			     in
-			       (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
+			       (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2',
 				mkProd (name, u1, t2')))
 		| _ -> raise NoCoercion))
 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index d7d304279a..49eab5d29d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -159,7 +159,7 @@ let list_of_local_binders l =
 
 let lift_binders k n l =
   let rec aux n = function
-    | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+    | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl
     | [] -> []
   in aux n l
 
@@ -326,7 +326,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 
 let nf_evar_context isevars ctx = 
   List.map (fun (n, b, t) -> 
-    (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
+    (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
     
 let build_mutrec lnameargsardef boxed = 
   let sigma = Evd.empty and env = Global.env () in 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 769aff9dcf..5e7f025be1 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -58,7 +58,7 @@ let subst_deps obls deps t =
        let xobl = obls.(x) in
 	 debug 3 (str "Trying to get body of obligation " ++ int x);
        let oblb = 
-	 try out_some xobl.obl_body
+	 try Option.get xobl.obl_body
 	 with _ ->
 	   debug 3 (str "Couldn't get body of obligation " ++ int x);
 	   assert(false)
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index ab542feb20..0ed0632c65 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -290,7 +290,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
 		      let tycon = 
-			option_map 
+			Option.map 
 			  (fun (abs, ty) ->
 			     match abs with
 				 None ->
@@ -306,7 +306,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
 			    uj_type = nf_isevar !isevars typ' }
-			  (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
+			  (Option.map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
 
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
@@ -314,7 +314,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in
+	let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in
 	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
 	let resj =
 	  match kind_of_term resj.uj_val with
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 1aabd4348e..82d7c19e51 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -691,11 +691,11 @@ let _ =
              Buffer.output_buffer ch theory_buffer ;
              close_out ch
        end ;
-       Util.option_iter 
+       Option.iter 
 	(fun fn ->
 	  let coqdoc = Coq_config.bindir^"/coqdoc" in
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
-	  let dir = Util.out_some xml_library_root in
+	  let dir = Option.get xml_library_root in
           let command cmd =
            if Sys.command cmd <> 0 then
             Util.anomaly ("Error executing \"" ^ cmd ^ "\"")