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

4 files changed, 16 insertions, 16 deletions

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