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

11 files changed, 88 insertions, 88 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index a3ac17b34..8bce850db 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -297,7 +297,7 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
   let trans_clenv clenv = Clenv.subst_clenv subst clenv in
   let trans_data data code = 	      
     { data with
-	pat = option_smartmap (subst_pattern subst) data.pat ;
+	pat = Option.smartmap (subst_pattern subst) data.pat ;
 	code = code ;
     }
   in
@@ -637,7 +637,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 = 
@@ -781,7 +781,7 @@ let gen_auto n lems dbnames =
   | None -> full_auto n lems
   | Some l -> auto n lems l
 
-let inj_or_var = option_map (fun n -> ArgArg n)
+let inj_or_var = Option.map (fun n -> ArgArg n)
 
 let h_auto n lems l =
   Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map inj_open lems,l))
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index ec8a38501..771dbe736 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -25,10 +25,10 @@ open Pp
 let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) 
 
 let intern_justification_items globs = 
-  option_map (List.map (intern_constr globs))
+  Option.map (List.map (intern_constr globs))
 
 let intern_justification_method globs = 
-  option_map (intern_tactic globs)
+  Option.map (intern_tactic globs)
 
 let intern_statement intern_it globs st =
   {st_label=st.st_label;
@@ -52,7 +52,7 @@ let add_name nam globs=
 
 let intern_hyp iconstr globs = function 
     Hvar (loc,(id,topt)) -> add_var id globs,
-      Hvar (loc,(id,option_map (intern_constr globs) topt))
+      Hvar (loc,(id,Option.map (intern_constr globs) topt))
   | Hprop st -> add_name st.st_label globs,
       Hprop (intern_statement iconstr globs st)
 
@@ -73,7 +73,7 @@ let intern_casee globs = function
 let intern_hyp_list args globs =
   let intern_one globs (loc,(id,opttyp)) =
     (add_var id globs),
-    (loc,(id,option_map (intern_constr globs) opttyp)) in
+    (loc,(id,Option.map (intern_constr globs) opttyp)) in
   list_fold_map intern_one globs args 
 
 let intern_suffices_clause globs (hyps,c) = 
@@ -141,7 +141,7 @@ let rec intern_proof_instr globs instr=
 (* INTERP *)
 
 let interp_justification_items sigma env =
-    option_map (List.map (fun c ->understand sigma env (fst c)))
+    Option.map (List.map (fun c ->understand sigma env (fst c)))
 
 let interp_constr check_sort sigma env c = 
   if check_sort then 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index b62bf5820..7a6b07d38 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -94,7 +94,7 @@ let e_split = e_constructor_tac (Some 1) 1
 TACTIC EXTEND econstructor
   [ "econstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ]
 | [ "econstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ]
-| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_map Tacinterp.eval_tactic t) ] 
+| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (Option.map Tacinterp.eval_tactic t) ] 
       END
 
 TACTIC EXTEND eleft
@@ -192,7 +192,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 -> conclPattern concl 
-	       (out_some p) tacast
+	       (Option.get p) tacast
        in 
        (tac,fmt_autotactic t))
        (*i
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 4a6c2ffb2..48d4afbc1 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -221,7 +221,7 @@ END
 
 let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = 
   {Tacexpr.onhyps=
-   Util.option_map 
+   Option.map 
      (fun l -> 
 	List.map 
 	  (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp))
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 787847400..3ddb4188b 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -23,7 +23,7 @@ open Equality
 
 TACTIC EXTEND replace 
    ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
--> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Util.option_map Tacinterp.eval_tactic tac) ]
+-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Option.map Tacinterp.eval_tactic tac) ]
 END
 
 TACTIC EXTEND replace_term_left
@@ -152,21 +152,21 @@ open Setoid_replace
 
 TACTIC EXTEND setoid_replace
    [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] ->
-     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ]
+     [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ]
  | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] ->
-     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ]
+     [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ]
  | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] ->
-     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ]
+     [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ]
  | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] ->
-     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ]
+     [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ]
  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] ->
-     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ]
+     [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ]
  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] ->
-     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ]
+     [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ]
  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] ->
-     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ]
+     [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ]
  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] ->
-     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ]
+     [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ]
 END
 
 TACTIC EXTEND setoid_rewrite
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 8bb7c5c2c..f5c54a533 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -30,7 +30,7 @@ let inj_occ (occ,c) = (occ,inj_open c)
 
 (* Basic tactics *)
 let h_intro_move x y =
-  abstract_tactic (TacIntroMove (x, option_map inj_id y)) (intro_move x y)
+  abstract_tactic (TacIntroMove (x, Option.map inj_id y)) (intro_move x y)
 let h_intro x        = h_intro_move (Some x) None
 let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
 let h_assumption     = abstract_tactic TacAssumption assumption
@@ -43,7 +43,7 @@ let h_apply ev cb    =
   abstract_tactic (TacApply (ev,inj_open_wb cb))
     (apply_with_ebindings_gen ev cb)
 let h_elim ev cb cbo    =
-  abstract_tactic (TacElim (ev,inj_open_wb cb,option_map inj_open_wb cbo))
+  abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo))
     (elim ev cb cbo)
 let h_elim_type c    = abstract_tactic (TacElimType (inj_open c)) (elim_type c)
 let h_case ev cb     = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb)
@@ -78,10 +78,10 @@ let h_simple_induction h =
 let h_simple_destruct h  =
   abstract_tactic (TacSimpleDestruct h) (simple_destruct h)
 let h_new_induction ev c e idl =
-  abstract_tactic (TacNewInduction (ev,List.map inj_ia c,option_map inj_open_wb e,idl))
+  abstract_tactic (TacNewInduction (ev,List.map inj_ia c,Option.map inj_open_wb e,idl))
     (new_induct ev c e idl)
 let h_new_destruct ev c e idl =
-  abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,option_map inj_open_wb e,idl))
+  abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl))
     (new_destruct ev c e idl)
 let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d)
 let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c)
@@ -113,8 +113,8 @@ let h_simplest_right  = h_right NoBindings
 let h_reduce r cl  = 
   abstract_tactic (TacReduce (inj_red_expr r,cl)) (reduce r cl)
 let h_change oc c cl =
-  abstract_tactic (TacChange (option_map inj_occ oc,inj_open c,cl))
-    (change (option_map Redexpr.out_with_occurrences oc) c cl)
+  abstract_tactic (TacChange (Option.map inj_occ oc,inj_open c,cl))
+    (change (Option.map Redexpr.out_with_occurrences oc) c cl)
 
 (* Equivalence relations *)
 let h_reflexivity    = abstract_tactic TacReflexivity intros_reflexivity
diff --git a/tactics/inv.ml b/tactics/inv.ml
index bfaa7e5e4..d8d7661be 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -385,7 +385,7 @@ let rec get_names allow_conj = function
   | IntroOrAndPattern [l] -> 
       if allow_conj then
 	if l = [] then (None,[]) else
-	  let l = List.map (fun id -> out_some (fst (get_names false id))) l in
+	  let l = List.map (fun id -> Option.get (fst (get_names false id))) l in
 	  (Some (List.hd l), l)
       else
 	error "Nested conjunctive patterns not allowed for inversion equations"
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index d53ca6126..c53a5088a 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -43,14 +43,14 @@ let get_dn dnm hkey =
   try Gmap.find hkey dnm with Not_found -> Btermdn.create ()
 
 let add dn (na,(pat,valu)) =
-  let hkey = option_map fst (Termdn.constr_pat_discr pat) in 
+  let hkey = Option.map fst (Termdn.constr_pat_discr pat) in 
   dn.table <- Gmap.add na (pat,valu) dn.table;
   let dnm = dn.patterns in
   dn.patterns <- Gmap.add hkey (Btermdn.add (get_dn dnm hkey) (pat,valu)) dnm
     
 let rmv dn na =
   let (pat,valu) = Gmap.find na dn.table in
-  let hkey = option_map fst (Termdn.constr_pat_discr pat) in 
+  let hkey = Option.map fst (Termdn.constr_pat_discr pat) in 
   dn.table <- Gmap.remove na dn.table;
   let dnm = dn.patterns in
   dn.patterns <- Gmap.add hkey (Btermdn.rmv (get_dn dnm hkey) (pat,valu)) dnm
@@ -62,7 +62,7 @@ let remap ndn na (pat,valu) =
   add ndn (na,(pat,valu))
 
 let lookup dn valu =
-  let hkey = option_map fst (Termdn.constr_val_discr valu) in 
+  let hkey = Option.map fst (Termdn.constr_val_discr valu) in 
   try Btermdn.lookup (Gmap.find hkey  dn.patterns) valu with Not_found -> []
 
 let app f dn = Gmap.iter f dn.table
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 36ef9be47..307968116 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -85,7 +85,7 @@ type morphism_class =
 let subst_mps_in_relation_class subst =
  function
     Relation  t -> Relation  (subst_mps subst t)
-  | Leibniz t -> Leibniz (option_map (subst_mps subst) t) 
+  | Leibniz t -> Leibniz (Option.map (subst_mps subst) t) 
 
 let subst_mps_in_argument_class subst (variance,rel) =
  variance, subst_mps_in_relation_class subst rel
@@ -297,9 +297,9 @@ let relation_morphism_of_constr_morphism =
 let subst_relation subst relation = 
   let rel_a' = subst_mps subst relation.rel_a in
   let rel_aeq' = subst_mps subst relation.rel_aeq in
-  let rel_refl' = option_map (subst_mps subst) relation.rel_refl in
-  let rel_sym' = option_map (subst_mps subst) relation.rel_sym in
-  let rel_trans' = option_map (subst_mps subst) relation.rel_trans in
+  let rel_refl' = Option.map (subst_mps subst) relation.rel_refl in
+  let rel_sym' = Option.map (subst_mps subst) relation.rel_sym in
+  let rel_trans' = Option.map (subst_mps subst) relation.rel_trans in
   let rel_X_relation_class' = subst_mps subst relation.rel_X_relation_class in
   let rel_Xreflexive_relation_class' =
    subst_mps subst relation.rel_Xreflexive_relation_class
@@ -640,9 +640,9 @@ let apply_to_relation subst rel =
    assert (new_quantifiers_no >= 0) ;
    { rel_a = mkApp (rel.rel_a, subst) ;
      rel_aeq = mkApp (rel.rel_aeq, subst) ;
-     rel_refl = option_map (fun c -> mkApp (c,subst)) rel.rel_refl ; 
-     rel_sym = option_map (fun c -> mkApp (c,subst)) rel.rel_sym;
-     rel_trans = option_map (fun c -> mkApp (c,subst)) rel.rel_trans;
+     rel_refl = Option.map (fun c -> mkApp (c,subst)) rel.rel_refl ; 
+     rel_sym = Option.map (fun c -> mkApp (c,subst)) rel.rel_sym;
+     rel_trans = Option.map (fun c -> mkApp (c,subst)) rel.rel_trans;
      rel_quantifiers_no = new_quantifiers_no;
      rel_X_relation_class = mkApp (rel.rel_X_relation_class, subst);
      rel_Xreflexive_relation_class =
@@ -1012,9 +1012,9 @@ let int_add_relation id a aeq refl sym trans =
  let env = Global.env () in
  let a_quantifiers_rev = check_a env a in
   check_eq env a_quantifiers_rev a aeq  ;
-  option_iter (check_refl env a_quantifiers_rev a aeq) refl ;
-  option_iter (check_sym env a_quantifiers_rev a aeq) sym ;
-  option_iter (check_trans env a_quantifiers_rev a aeq) trans ;
+  Option.iter (check_refl env a_quantifiers_rev a aeq) refl ;
+  Option.iter (check_sym env a_quantifiers_rev a aeq) sym ;
+  Option.iter (check_trans env a_quantifiers_rev a aeq) trans ;
   let quantifiers_no = List.length a_quantifiers_rev in
   let aeq_rel =
    { rel_a = a;
@@ -1075,9 +1075,9 @@ let int_add_relation id a aeq refl sym trans =
       let a_instance = apply_to_rels a a_quantifiers_rev in
       let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
       let sym_instance =
-       option_map (fun x -> apply_to_rels x a_quantifiers_rev) sym in
+       Option.map (fun x -> apply_to_rels x a_quantifiers_rev) sym in
       let refl_instance =
-       option_map (fun x -> apply_to_rels x a_quantifiers_rev) refl in
+       Option.map (fun x -> apply_to_rels x a_quantifiers_rev) refl in
       let trans_instance = apply_to_rels trans a_quantifiers_rev in
       let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output =
        match sym_instance, refl_instance with
@@ -1132,8 +1132,8 @@ let int_add_relation id a aeq refl sym trans =
 (* The vernac command "Add Relation ..." *)
 let add_relation id a aeq refl sym trans =
   Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"];
-  int_add_relation id (constr_of a) (constr_of aeq) (option_map constr_of refl)
-    (option_map constr_of sym) (option_map constr_of trans)
+  int_add_relation id (constr_of a) (constr_of aeq) (Option.map constr_of refl)
+    (Option.map constr_of sym) (Option.map constr_of trans)
 
 (************************ Add Setoid ******************************************)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 11d86630b..09d9fe8d7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -550,7 +550,7 @@ let intern_red_expr ist = function
   | Cbv f -> Cbv (intern_flag ist f)
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l)
-  | Simpl o -> Simpl (option_map (intern_constr_occurrence ist) o)
+  | Simpl o -> Simpl (Option.map (intern_constr_occurrence ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
   
 
@@ -559,7 +559,7 @@ let intern_inversion_strength lf ist = function
       NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
       intern_intro_pattern lf ist ids)
   | DepInversion (k,copt,ids) ->
-      DepInversion (k, option_map (intern_constr ist) copt,
+      DepInversion (k, Option.map (intern_constr ist) copt,
       intern_intro_pattern lf ist ids)
   | InversionUsing (c,idl) ->
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
@@ -654,8 +654,8 @@ let rec intern_atomic lf ist x =
       TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
   | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
-      TacIntroMove (option_map (intern_ident lf ist) ido,
-          option_map (intern_hyp ist) ido')
+      TacIntroMove (Option.map (intern_ident lf ist) ido,
+          Option.map (intern_hyp ist) ido')
   | TacAssumption -> TacAssumption
   | TacExact c -> TacExact (intern_constr ist c)
   | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
@@ -663,21 +663,21 @@ let rec intern_atomic lf ist x =
   | TacApply (ev,cb) -> TacApply (ev,intern_constr_with_bindings ist cb)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,intern_constr_with_bindings ist cb,
-               option_map (intern_constr_with_bindings ist) cbo)
+               Option.map (intern_constr_with_bindings ist) cbo)
   | TacElimType c -> TacElimType (intern_type ist c)
   | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
   | TacCaseType c -> TacCaseType (intern_type ist c)
-  | TacFix (idopt,n) -> TacFix (option_map (intern_ident lf ist) idopt,n)
+  | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
       TacMutualFix (intern_ident lf ist id, n, List.map f l)
-  | TacCofix idopt -> TacCofix (option_map (intern_ident lf ist) idopt)
+  | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
   | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
-      TacAssert (option_map (intern_tactic ist) otac,
+      TacAssert (Option.map (intern_tactic ist) otac,
                  intern_intro_pattern lf ist ipat,
                  intern_constr_gen (otac<>None) ist c)
   | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
@@ -690,14 +690,14 @@ let rec intern_atomic lf ist x =
   (* Automation tactics *)
   | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
   | TacAuto (n,lems,l) ->
-      TacAuto (option_map (intern_or_var ist) n,
+      TacAuto (Option.map (intern_or_var ist) n,
         List.map (intern_constr ist) lems,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
   | TacDAuto (n,p,lems) ->
-      TacDAuto (option_map (intern_or_var ist) n,p,
+      TacDAuto (Option.map (intern_or_var ist) n,p,
         List.map (intern_constr ist) lems)
 
   (* Derived basic tactics *)
@@ -705,13 +705,13 @@ let rec intern_atomic lf ist x =
       TacSimpleInduction (intern_quantified_hypothesis ist h)
   | TacNewInduction (ev,lc,cbo,ids) ->
       TacNewInduction (ev,List.map (intern_induction_arg ist) lc,
-               option_map (intern_constr_with_bindings ist) cbo,
+               Option.map (intern_constr_with_bindings ist) cbo,
                (intern_intro_pattern lf ist ids))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (ev,c,cbo,ids) ->
       TacNewDestruct (ev,List.map (intern_induction_arg ist) c,
-               option_map (intern_constr_with_bindings ist) cbo,
+               Option.map (intern_constr_with_bindings ist) cbo,
 	       (intern_intro_pattern lf ist ids))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
@@ -738,14 +738,14 @@ let rec intern_atomic lf ist x =
   | TacLeft bl -> TacLeft (intern_bindings ist bl)
   | TacRight bl -> TacRight (intern_bindings ist bl)
   | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl)
-  | TacAnyConstructor t -> TacAnyConstructor (option_map (intern_tactic ist) t)
+  | TacAnyConstructor t -> TacAnyConstructor (Option.map (intern_tactic ist) t)
   | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl)
 
   (* Conversion *)
   | TacReduce (r,cl) ->
       TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
   | TacChange (occl,c,cl) ->
-      TacChange (option_map (intern_constr_occurrence ist) occl,
+      TacChange (Option.map (intern_constr_occurrence ist) occl,
         (if occl = None then intern_type ist c else intern_constr ist c),
 	clause_app (intern_hyp_location ist) cl)
 
@@ -791,7 +791,7 @@ and intern_tactic_seq ist = function
   | TacLetIn (l,u) ->
       let l = List.map
         (fun (n,c,b) ->
-          (n,option_map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
+          (n,Option.map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
       let (l1,l2) = ist.ltacvars in
       let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
       ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
@@ -1248,7 +1248,7 @@ let interp_hyp_location ist gl ((occs,id),hl) =
   ((interp_int_or_var_list ist occs,interp_hyp ist gl id),hl)
 
 let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
-  { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol;
+  { onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol;
     onconcl=b;
     concl_occs= interp_int_or_var_list ist occs }
 
@@ -1440,7 +1440,7 @@ let interp_red_expr ist sigma env = function
   | Cbv f -> Cbv (interp_flag ist env f)
   | Lazy f -> Lazy (interp_flag ist env f)
   | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
-  | Simpl o -> Simpl (option_map (interp_pattern ist sigma env) o)
+  | Simpl o -> Simpl (Option.map (interp_pattern ist sigma env) o)
   | (Red _ |  Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl)
@@ -2037,8 +2037,8 @@ and interp_atomic ist gl = function
   | TacIntrosUntil hyp ->
       h_intros_until (interp_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
-      h_intro_move (option_map (interp_fresh_ident ist gl) ido)
-      (option_map (interp_hyp ist gl) ido')
+      h_intro_move (Option.map (interp_fresh_ident ist gl) ido)
+      (Option.map (interp_hyp ist gl) ido')
   | TacAssumption -> h_assumption
   | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
   | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
@@ -2046,15 +2046,15 @@ and interp_atomic ist gl = function
   | TacApply (ev,cb) -> h_apply ev (interp_constr_with_bindings ist gl cb)
   | TacElim (ev,cb,cbo) ->
       h_elim ev (interp_constr_with_bindings ist gl cb)
-                (option_map (interp_constr_with_bindings ist gl) cbo)
+                (Option.map (interp_constr_with_bindings ist gl) cbo)
   | TacElimType c -> h_elim_type (pf_interp_type ist gl c)
   | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb)
   | TacCaseType c -> h_case_type (pf_interp_type ist gl c)
-  | TacFix (idopt,n) -> h_fix (option_map (interp_fresh_ident ist gl) idopt) n
+  | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c)
       in h_mutual_fix (interp_fresh_ident ist gl id) n (List.map f l)
-  | TacCofix idopt -> h_cofix (option_map (interp_fresh_ident ist gl) idopt)
+  | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt)
   | TacMutualCofix (id,l) ->
       let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in
       h_mutual_cofix (interp_fresh_ident ist gl id) (List.map f l)
@@ -2062,7 +2062,7 @@ and interp_atomic ist gl = function
   | TacAssert (t,ipat,c) ->
       let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
       abstract_tactic (TacAssert (t,ipat,inj_open c))
-        (Tactics.forward (option_map (interp_tactic ist) t)
+        (Tactics.forward (Option.map (interp_tactic ist) t)
 	  (interp_intro_pattern ist gl ipat) c)
   | TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
@@ -2073,17 +2073,17 @@ and interp_atomic ist gl = function
   (* Automation tactics *)
   | TacTrivial (lems,l) -> 
       Auto.h_trivial (pf_interp_constr_list ist gl lems)
-	(option_map (List.map (interp_hint_base ist)) l)
+	(Option.map (List.map (interp_hint_base ist)) l)
   | TacAuto (n,lems,l) ->
-      Auto.h_auto (option_map (interp_int_or_var ist) n)
+      Auto.h_auto (Option.map (interp_int_or_var ist) n)
       (pf_interp_constr_list ist gl lems)
-      (option_map (List.map (interp_hint_base ist)) l)
+      (Option.map (List.map (interp_hint_base ist)) l)
   | TacAutoTDB n -> Dhyp.h_auto_tdb n
   | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
   | TacDestructConcl -> Dhyp.h_destructConcl
   | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
   | TacDAuto (n,p,lems) ->
-      Auto.h_dauto (option_map (interp_int_or_var ist) n,p)
+      Auto.h_dauto (Option.map (interp_int_or_var ist) n,p)
       (pf_interp_constr_list ist gl lems)
 
   (* Derived basic tactics *)
@@ -2091,13 +2091,13 @@ and interp_atomic ist gl = function
       h_simple_induction (interp_quantified_hypothesis ist h)
   | TacNewInduction (ev,lc,cbo,ids) ->
       h_new_induction ev (List.map (interp_induction_arg ist gl) lc)
-        (option_map (interp_constr_with_bindings ist gl) cbo)
+        (Option.map (interp_constr_with_bindings ist gl) cbo)
         (interp_intro_pattern ist gl ids)
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist h)
   | TacNewDestruct (ev,c,cbo,ids) -> 
       h_new_destruct ev (List.map (interp_induction_arg ist gl) c)
-        (option_map (interp_constr_with_bindings ist gl) cbo)
+        (Option.map (interp_constr_with_bindings ist gl) cbo)
         (interp_intro_pattern ist gl ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
@@ -2128,7 +2128,7 @@ and interp_atomic ist gl = function
   | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl)
   | TacAnyConstructor t ->
       abstract_tactic (TacAnyConstructor t)
-        (Tactics.any_constructor (option_map (interp_tactic ist) t))
+        (Tactics.any_constructor (Option.map (interp_tactic ist) t))
   | TacConstructor (n,bl) ->
       h_constructor (skip_metaid n) (interp_bindings ist gl bl)
 
@@ -2136,7 +2136,7 @@ and interp_atomic ist gl = function
   | TacReduce (r,cl) ->
       h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl)
   | TacChange (occl,c,cl) ->
-      h_change (option_map (pf_interp_pattern ist gl) occl)
+      h_change (Option.map (pf_interp_pattern ist gl) occl)
         (if occl = None then pf_interp_type ist gl c 
 	 else pf_interp_constr ist gl c)
         (interp_clause ist gl cl)
@@ -2152,7 +2152,7 @@ and interp_atomic ist gl = function
 	(List.map (fun (b,c) -> (b, interp_constr_with_bindings ist gl c)) l)
 	(interp_clause ist gl cl)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
-      Inv.dinv k (option_map (pf_interp_constr ist gl) c)
+      Inv.dinv k (Option.map (pf_interp_constr ist gl) c)
         (interp_intro_pattern ist gl ids)
         (interp_declared_or_quantified_hypothesis ist gl hyp)
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
@@ -2201,7 +2201,7 @@ and interp_atomic ist gl = function
     | ExtraArgType s when tactic_genarg_level s <> None ->
           (* Special treatment of tactic arguments *)
 	val_interp ist gl 
-          (out_gen (globwit_tactic (out_some (tactic_genarg_level s))) x)
+          (out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x)
     | List0ArgType ConstrArgType -> 
         let wit = wit_list0 globwit_constr in
         VList (List.map (mk_constr_value ist gl) (out_gen wit x))
@@ -2348,7 +2348,7 @@ let subst_redexp subst = function
   | Cbv f -> Cbv (subst_flag subst f)
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l)
-  | Simpl o -> Simpl (option_map (subst_constr_occurrence subst) o)
+  | Simpl o -> Simpl (Option.map (subst_constr_occurrence subst) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let subst_raw_may_eval subst = function
@@ -2377,7 +2377,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacApply (ev,cb) -> TacApply (ev,subst_raw_with_bindings subst cb)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,subst_raw_with_bindings subst cb,
-               option_map (subst_raw_with_bindings subst) cbo)
+               Option.map (subst_raw_with_bindings subst) cbo)
   | TacElimType c -> TacElimType (subst_rawconstr subst c)
   | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb)
   | TacCaseType c -> TacCaseType (subst_rawconstr subst c)
@@ -2389,7 +2389,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
   | TacCut c -> TacCut (subst_rawconstr subst c)
   | TacAssert (b,na,c) ->
-      TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c)
+      TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c)
   | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
   | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)
@@ -2407,11 +2407,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacSimpleInduction h as x -> x
   | TacNewInduction (ev,lc,cbo,ids) ->
       TacNewInduction (ev,List.map (subst_induction_arg subst) lc,
-               option_map (subst_raw_with_bindings subst) cbo, ids)
+               Option.map (subst_raw_with_bindings subst) cbo, ids)
   | TacSimpleDestruct h as x -> x
   | TacNewDestruct (ev,c,cbo,ids) ->
       TacNewDestruct (ev,List.map (subst_induction_arg subst) c,
-               option_map (subst_raw_with_bindings subst) cbo, ids)
+               Option.map (subst_raw_with_bindings subst) cbo, ids)
   | TacDoubleInduction (h1,h2) as x -> x
   | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
   | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
@@ -2431,13 +2431,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacLeft bl -> TacLeft (subst_bindings subst bl)
   | TacRight bl -> TacRight (subst_bindings subst bl)
   | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl)
-  | TacAnyConstructor t -> TacAnyConstructor (option_map (subst_tactic subst) t)
+  | TacAnyConstructor t -> TacAnyConstructor (Option.map (subst_tactic subst) t)
   | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl)
 
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
   | TacChange (occl,c,cl) ->
-      TacChange (option_map (subst_constr_occurrence subst) occl,
+      TacChange (Option.map (subst_constr_occurrence subst) occl,
         subst_rawconstr subst c, cl)
 
   (* Equivalence relations *)
@@ -2450,7 +2450,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 		  List.map (fun (b,c) ->b,subst_raw_with_bindings subst c) l,
 		  cl)
   | TacInversion (DepInversion (k,c,l),hyp) ->
-     TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp)
+     TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp)
   | TacInversion (NonDepInversion _,_) as x -> x
   | TacInversion (InversionUsing (c,cl),hyp) ->
       TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp)
@@ -2469,7 +2469,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in
       TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr))
   | TacLetIn (l,u) ->
-      let l = List.map (fun (n,c,b) -> (n,option_map (subst_tactic subst) c,subst_tacarg subst b)) l in
+      let l = List.map (fun (n,c,b) -> (n,Option.map (subst_tactic subst) c,subst_tacarg subst b)) l in
       TacLetIn (l,subst_tactic subst u)
   | TacMatchContext (lz,lr,lmr) ->
       TacMatchContext(lz,lr, subst_match_rule subst lmr)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3121d3a49..782f2a4c1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -60,7 +60,7 @@ let inj_open c = (Evd.empty,c)
 let inj_occ (occ,c) = (occ,inj_open c)
 
 let inj_red_expr = function
-  | Simpl lo -> Simpl (option_map inj_occ lo)
+  | Simpl lo -> Simpl (Option.map inj_occ lo)
   | Fold l -> Fold (List.map inj_open l)
   | Pattern l -> Pattern (List.map inj_occ l)
   | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c)
@@ -1694,7 +1694,7 @@ let mkHRefl t x =
 	[| t; x |])
 
 let mkCoe a x p px y eq = 
-  mkApp (out_some (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |])
+  mkApp (Option.get (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |])
 
 let lift_togethern n l =
   let l', _ =