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

10 files changed, 20 insertions, 20 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index e28890cee7..b2c279b39c 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -160,7 +160,7 @@ type grammar_tactic_production =
 
 let make_prod_item = function
   | TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
-  | TacNonTerm (_,(nont,t), po) -> (nont, option_map (fun p -> (p,t)) po)
+  | TacNonTerm (_,(nont,t), po) -> (nont, Option.map (fun p -> (p,t)) po)
 
 (* Tactic grammar extensions *)
 
@@ -194,7 +194,7 @@ let extend_vernac_command_grammar s gl =
 let find_index s t =
   let t,n = repr_ident (id_of_string t) in
   if s <> t or n = None then raise Not_found;
-  out_some n
+  Option.get n
 
 let rec interp_entry_name up_level s =
   let l = String.length s in
@@ -233,7 +233,7 @@ let make_vprod_item n = function
   | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
   | VNonTerm (loc, nt, po) ->
       let (etyp, e) = interp_entry_name n nt in
-      e, option_map (fun p -> (p,etyp)) po
+      e, Option.map (fun p -> (p,etyp)) po
 
 let get_tactic_entry n =
   if n = 0 then
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml
index ac54fc63d5..717abaa66a 100644
--- a/parsing/g_ascii_syntax.ml
+++ b/parsing/g_ascii_syntax.ml
@@ -72,7 +72,7 @@ let make_ascii_string n =
   if n>=32 && n<=126 then String.make 1 (char_of_int n)
   else Printf.sprintf "%03d" n
 
-let uninterp_ascii_string r = option_map make_ascii_string (uninterp_ascii r)
+let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r)
 
 let _ =
   Notation.declare_string_interpreter "char_scope"
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 04e0f84ca3..4627d23052 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -59,7 +59,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   (snd id,(n,ro),bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
-  let _ = option_map (fun (aloc,_) ->
+  let _ = Option.map (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofixb",
        Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9b21837d8b..23e4ba6218 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -104,7 +104,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
   (id,n,CProdN(loc,bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
-  let _ = option_map (fun (aloc,_) ->
+  let _ = Option.map (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofix_tac",
        Pp.str"Annotation forbidden in cofix expression")) ann in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a64cf74cc7..a7a78f7700 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -274,8 +274,8 @@ GEXTEND Gram
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
-      | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CWfRec rel) 
-      | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CMeasureRec rel) 
+      | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CWfRec rel) 
+      | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CMeasureRec rel) 
       | ->  (None, CStructRec)
       ] ]
   ;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d72a490467..07055869af 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -576,7 +576,7 @@ let find_position forpat other assoc lev =
         | (p,_ as pa)::l when p > n -> pa :: add_level (Some p) l
         | (p,a)::l when p = n ->
 	    if admissible_assoc (a,assoc) then raise Exit;
-	    error_level_assoc p a (out_some assoc)
+	    error_level_assoc p a (Option.get assoc)
 	| l -> after := q; (n,create_assoc assoc)::l
       in
       try
@@ -587,7 +587,7 @@ let find_position forpat other assoc lev =
         level_stack := updated:: !level_stack;
 	let assoc = create_assoc assoc in
 	(if !after = None then Some Gramext.First
-	else Some (Gramext.After (constr_level (out_some !after)))),
+	else Some (Gramext.After (constr_level (Option.get !after)))),
 	Some assoc, Some (constr_level n)
       with
           Exit ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 1c9eb1e2a2..8e542ce147 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -386,12 +386,12 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
       match ro with
 	  CStructRec ->
 	    if List.length ids > 1 && n <> None then 
-	      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
+	      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
 	    else mt() 
 	| CWfRec c ->
-	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
+	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
 	| CMeasureRec c ->
-	    spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
+	    spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
   in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
@@ -428,7 +428,7 @@ let pr_case_item pr (tm,(na,indnalopt)) =
     | Name id when not (is_var id tm) -> spc () ++ str "as " ++  pr_id id
     | Anonymous when tm_clash (tm,indnalopt) <> None ->
 	(* hide [tm] name to avoid conflicts *)
-	spc () ++ str "as _" (* ++ pr_id (out_some (tm_clash (tm,indnalopt)))*)
+	spc () ++ str "as _" (* ++ pr_id (Option.get (tm_clash (tm,indnalopt)))*)
     | _ -> mt ()) ++
 *)
   (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index a5bcea6f1b..bbb481f3e2 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -747,7 +747,7 @@ let rec pr_vernac = function
 	prlist (function None -> str " _"
                        | Some id -> spc () ++ pr_id id) idl
 	++ str" :=" ++ brk(1,1) ++
-	let idl = List.map out_some (List.filter (fun x -> not (x=None)) idl)in
+	let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in
         pr_raw_tactic_env 
 	  (idl @ List.map snd (List.map fst l))
 	  (Global.env())
@@ -794,7 +794,7 @@ let rec pr_vernac = function
           spc() ++ str"in" ++ spc () ++ pr_constr c)
       | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) 
       in 
-      (if io = None then mt() else int (out_some io) ++ str ": ") ++ 
+      (if io = None then mt() else int (Option.get io) ++ str ": ") ++ 
       pr_mayeval r c
   | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
   | VernacPrint p -> 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index a2341edb1e..a3a0c2f152 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -456,10 +456,10 @@ let gallina_print_leaf_entry with_values c =
 
 let gallina_print_context with_values = 
   let rec prec n = function
-    | h::rest when n = None or out_some n > 0 -> 
+    | h::rest when n = None or Option.get n > 0 -> 
 	(match gallina_print_library_entry with_values h with
 	  | None -> prec n rest
-	  | Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ())
+	  | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
     | _ -> mt ()
   in 
   prec
diff --git a/parsing/search.ml b/parsing/search.ml
index b9982ad3d2..fd9eb12bbb 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -52,7 +52,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
 	(try 
 	   let (idc,_,typ) = get_variable (basename sp) in 
            if refopt = None
-	     || head_const typ = constr_of_global (out_some refopt)
+	     || head_const typ = constr_of_global (Option.get refopt)
 	   then
 	     fn (VarRef idc) env typ
 	 with Not_found -> (* we are in a section *) ())
@@ -60,7 +60,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
 	let cst = locate_constant (qualid_of_sp sp) in
 	let typ = Typeops.type_of_constant env cst in
         if refopt = None
-	  || head_const typ = constr_of_global (out_some refopt)
+	  || head_const typ = constr_of_global (Option.get refopt)
 	then
 	  fn (ConstRef cst) env typ
     | "INDUCTIVE" ->