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, 12 insertions, 12 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 6e9835487..65d08dd81 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -92,7 +92,7 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
         let (_,bd,ty) = Global.lookup_named id in
-        CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in
+        CheckedSectionLocalDef (Option.get bd,ty,cst,opaq) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id;
   Dischargedhypsmap.set_discharged_hyps sp [];
@@ -200,7 +200,7 @@ let hcons_constant_declaration = function
       let (hcons1_constr,_) = hcons_constr (hcons_names()) in
       DefinitionEntry
        { const_entry_body = hcons1_constr ce.const_entry_body;
-	 const_entry_type = option_map hcons1_constr ce.const_entry_type;
+	 const_entry_type = Option.map hcons1_constr ce.const_entry_type;
          const_entry_opaque = ce.const_entry_opaque; 
          const_entry_boxed = ce.const_entry_boxed }
   | cd -> cd
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 8bfc7ac85..6a73943b9 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -579,7 +579,7 @@ let register_library dir cenv objs digest =
 	  let msid,substitute,keep = objs in
 	  let substobjs = empty_subst, [], msid, substitute in
 	  let substituted = subst_substobjs dir mp substobjs in
-	  let objects = option_map (fun seg -> seg@keep) substituted in
+	  let objects = Option.map (fun seg -> seg@keep) substituted in
 	  let modobjs = substobjs, objects in
 	    Hashtbl.add library_cache dir modobjs;
 	    modobjs
diff --git a/library/impargs.ml b/library/impargs.ml
index 3085b00c0..479936c88 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -259,8 +259,8 @@ let compute_manual_implicits flags ref l =
 	with Not_found ->
 	l, None in
       let imps' = merge (k+1) l' imps in
-      let m = option_map (set_maximality imps') m in
-      option_map (set_implicit id imp) m :: imps'
+      let m = Option.map (set_maximality imps') m in
+      Option.map (set_implicit id imp) m :: imps'
   | (Anonymous,_imp)::imps -> 
       None :: merge (k+1) l imps
   | [] when l = [] -> []
diff --git a/library/lib.ml b/library/lib.ml
index 71494311e..50bef5a5d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -513,7 +513,7 @@ let open_section id =
 let discharge_item ((sp,_ as oname),e) =
   match e with
   | Leaf lobj ->
-      option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+      Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
   | FrozenState _ -> None
   | ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None
   | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ ->
@@ -539,7 +539,7 @@ let close_section id =
   if !Options.xml_export then !xml_close_section id;
   let newdecls = List.map discharge_item secdecls in
   Summary.section_unfreeze_summaries fs;
-  List.iter (option_iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
+  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
   Cooking.clear_cooking_sharing ();
   Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
diff --git a/library/libobject.ml b/library/libobject.ml
index 46cc55361..7c74d402b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -112,7 +112,7 @@ let declare_object odecl =
       anomaly "somehow we got the wrong dynamic object in the classifyfun"
   and discharge (oname,lobj) = 
     if Dyn.tag lobj = na then 
-      option_map infun (odecl.discharge_function (oname,outfun lobj))
+      Option.map infun (odecl.discharge_function (oname,outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the dischargefun"
   and rebuild lobj = 
@@ -120,7 +120,7 @@ let declare_object odecl =
     else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
   and exporter lobj = 
     if Dyn.tag lobj = na then 
-      option_map infun (odecl.export_function (outfun lobj))
+      Option.map infun (odecl.export_function (outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the exportfun"
 
diff --git a/library/library.ml b/library/library.ml
index 70eac95ae..ced150f7b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -496,7 +496,7 @@ let register_library (dir,m) =
   (* [needed] is the ordered list of libraries not already loaded *)
 let cache_require (_,(needed,modl,export)) =
   List.iter register_library needed;
-  option_iter (fun exp -> open_libraries exp (List.map find_library modl))
+  Option.iter (fun exp -> open_libraries exp (List.map find_library modl))
     export
 
 let load_require  _ (_,(needed,modl,_)) =
@@ -530,7 +530,7 @@ let require_library qidl export =
   let modrefl = List.map fst modrefl in
     if Lib.is_modtype () || Lib.is_module () then begin
       add_anonymous_leaf (in_require (needed,modrefl,None));
-      option_iter (fun exp ->
+      Option.iter (fun exp ->
 	List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
 	export
     end
@@ -544,7 +544,7 @@ let require_library_from_file idopt file export =
   let needed = List.rev needed in
   if Lib.is_modtype () || Lib.is_module () then begin
     add_anonymous_leaf (in_require (needed,[modref],None));
-    option_iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
+    Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
       export
   end
   else