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

6 files changed, 23 insertions, 23 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 933b23c53e..7546ad310b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -321,7 +321,7 @@ let init is_ide =
       set_vm_opt ();
       engage ();
       if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
-        option_iter Declaremods.start_library !toplevel_name;
+        Option.iter Declaremods.start_library !toplevel_name;
       init_library_roots ();
       load_vernac_obj ();
       require ();
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e25ff99e0c..bb30c669fc 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -320,7 +320,7 @@ let explain_hole_kind env = function
   | BinderType Anonymous ->
       str "the type of this anonymous binder"
   | ImplicitArg (c,(n,ido)) ->
-      let id = out_some ido in
+      let id = Option.get ido in
       str "the implicit parameter " ++
       pr_id id ++ spc () ++ str "of" ++
       spc () ++ Nametab.pr_global_env Idset.empty c
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 9a162997b6..7ebf3dfa9a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -763,21 +763,21 @@ let find_precedence lev etyps symbols =
 	| ETPattern | ETOther _ -> (* Give a default ? *)
 	    if lev = None then
 	      error "Need an explicit level"
-	    else out_some lev
+	    else Option.get lev
         | ETConstrList _ -> assert false (* internally used in grammar only *)
       with Not_found -> 
 	if lev = None then
 	  error "A left-recursive notation must have an explicit level"
-	else out_some lev)
+	else Option.get lev)
   | Terminal _ ::l when
       (match list_last symbols with Terminal _ -> true |_ -> false)
       -> 
       if lev = None then
 	(Options.if_verbose msgnl (str "Setting notation at level 0"); 0)
-      else out_some lev
+      else Option.get lev
   | _ ->
       if lev = None then error "Cannot determine the level";
-      out_some lev
+      Option.get lev
 
 let check_curly_brackets_notation_exists () =
   try let _ = Notation.level_of_notation "{ _ }" in ()
@@ -839,7 +839,7 @@ let compute_syntax_data (df,modifiers) =
 (* Registration of notations interpretation                            *)
 
 let load_notation _ (_,(_,scope,pat,onlyparse,_)) =
-  option_iter Notation.declare_scope scope
+  Option.iter Notation.declare_scope scope
 
 let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) =
   if i=1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 19fd343e57..e22b33e24c 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -54,7 +54,7 @@ let check c =
 
 let definition id ty c =
   let c = globalize [] c in
-  let ty = option_map (globalize []) ty in
+  let ty = Option.map (globalize []) ty in
   let ce = { const_entry_body = c; const_entry_type = ty } in
   let sp = make_path [] id CCI in
   env := add_constant sp ce (locals()) !env;
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index fbdc96d6e8..aba5aeb274 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -103,7 +103,7 @@ let get_bols_of_loc ibuf (bp,ep) =
         lines_rec ll nafter fl 
   in
   let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in
-  (fl,out_some ll)
+  (fl,Option.get ll)
 
 let dotted_location (b,e) =
   if e-b < 3 then 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d6b874c228..9cb2b26b73 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -298,7 +298,7 @@ let vernac_notation = Metasyntax.add_notation
 let start_proof_and_print idopt k t hook =
   start_proof_com idopt k t hook;
   print_subgoals ();
-  if !pcoq <> None then (out_some !pcoq).start_proof ()
+  if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
 let vernac_definition (local,_,_ as k) id def hook =
   match def with
@@ -386,7 +386,7 @@ let vernac_declare_module export id binders_ast mty_ast_o =
     Modintern.interp_modtype Modintern.interp_modexpr
      id binders_ast (Some mty_ast_o) None;
   if_verbose message ("Module "^ string_of_id id ^" is declared");
-  option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+  Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
 let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = 
   (* We check the state of the system (in section, in module type)
@@ -406,7 +406,7 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o =
 	  ("Interactive Module "^ string_of_id id ^" started") ;
         List.iter
          (fun (export,id) ->
-           option_iter
+           Option.iter
             (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
          ) argsexport
     | Some _ ->
@@ -422,13 +422,13 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o =
 	  id binders_ast mty_ast_o mexpr_ast_o;
 	if_verbose message 
 	  ("Module "^ string_of_id id ^" is defined");
-        option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
+        Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
          export
 
 let vernac_end_module export id =
   Declaremods.end_module id;
   if_verbose message ("Module "^ string_of_id id ^" is defined") ;
-  option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+  Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
 
 let vernac_declare_module_type id binders_ast mty_ast_o =
@@ -447,7 +447,7 @@ let vernac_declare_module_type id binders_ast mty_ast_o =
 	  ("Interactive Module Type "^ string_of_id id ^" started");
         List.iter
          (fun (export,id) ->
-           option_iter
+           Option.iter
             (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
          ) argsexport
 	  
@@ -542,7 +542,7 @@ let vernac_solve n tcom b =
     reset_top_of_script ()
   end;
   print_subgoals();
-  if !pcoq <> None then (out_some !pcoq).solve n
+  if !pcoq <> None then (Option.get !pcoq).solve n
 
   (* A command which should be a tactic. It has been
      added by Christine to patch an error in the design of the proof
@@ -910,12 +910,12 @@ let vernac_check_may_eval redexp glopt rc =
   let j = Typeops.typing env c in
   match redexp with
     | None ->
-	if !pcoq <> None then (out_some !pcoq).print_check env j
+	if !pcoq <> None then (Option.get !pcoq).print_check env j
 	else msg (print_judgment env j)
     | Some r ->
 	let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in
 	if !pcoq <> None
-	then (out_some !pcoq).print_eval redfun env evmap rc j
+	then (Option.get !pcoq).print_eval redfun env evmap rc j
 	else msg (print_eval redfun env evmap rc j)
 
   (* The same but avoiding the current goal context if any *)
@@ -940,7 +940,7 @@ let vernac_print = function
   | PrintMLLoadPath -> Mltop.print_ml_path ()
   | PrintMLModules -> Mltop.print_ml_modules ()
   | PrintName qid -> 
-      if !pcoq <> None then (out_some !pcoq).print_name qid
+      if !pcoq <> None then (Option.get !pcoq).print_name qid
       else msg (print_name qid)
   | PrintOpaqueName qid -> msg (print_opaque_name qid)
   | PrintGraph -> ppnl (Prettyp.print_graph())
@@ -995,7 +995,7 @@ let interp_search_about_item = function
 
 let vernac_search s r =
   let r = interp_search_restriction r in
-  if !pcoq <> None then (out_some !pcoq).search s r else
+  if !pcoq <> None then (Option.get !pcoq).search s r else
   match s with
   | SearchPattern c ->
       let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
@@ -1034,12 +1034,12 @@ let vernac_abort = function
   | None ->
       delete_current_proof ();
       if_verbose message "Current goal aborted";
-      if !pcoq <> None then (out_some !pcoq).abort ""
+      if !pcoq <> None then (Option.get !pcoq).abort ""
   | Some id ->
       delete_proof id;
       let s = string_of_id (snd id) in
       if_verbose message ("Goal "^s^" aborted");
-      if !pcoq <> None then (out_some !pcoq).abort s
+      if !pcoq <> None then (Option.get !pcoq).abort s
 
 let vernac_abort_all () =
   if refining() then begin
@@ -1109,7 +1109,7 @@ let explain_tree occ =
 
 let vernac_show = function
   | ShowGoal nopt ->
-      if !pcoq <> None then (out_some !pcoq).show_goal nopt
+      if !pcoq <> None then (Option.get !pcoq).show_goal nopt
       else msg (match nopt with
 	| None -> pr_open_subgoals ()
 	| Some n -> pr_nth_open_subgoal n)