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

1 files changed, 6 insertions, 6 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index aaab6a933f..d5de23bc5d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -133,7 +133,7 @@ let push_scopes = List.fold_right push_scope
 type local_scopes = tmp_scope_name option * scope_name list
 
 let make_current_scopes (tmp_scope,scopes) =
-  option_fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
+  Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
 
 (**********************************************************************)
 (* Delimiters *)
@@ -143,7 +143,7 @@ let delimiters_map = ref Gmap.empty
 let declare_delimiters scope key =
   let sc = find_scope scope in
   if sc.delimiters <> None && Options.is_verbose () then begin
-    let old = out_some sc.delimiters in
+    let old = Option.get sc.delimiters in
     Options.if_verbose 
       warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
   end;
@@ -239,12 +239,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x))
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
-    (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat)
+    (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
-    (patl, (fun r -> option_map mkString (uninterp r)), inpat)
+    (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.absolute_reference sp in ()
@@ -396,7 +396,7 @@ let uninterp_prim_token_cases_pattern c =
 let availability_of_prim_token printer_scope local_scopes =
   let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
   let scopes = make_current_scopes local_scopes in
-  option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
+  Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
 (* Miscellaneous *)
 
@@ -454,7 +454,7 @@ type arguments_scope_discharge_request =
   | ArgsScopeNoDischarge
 
 let load_arguments_scope _ (_,(_,r,scl)) =
-  List.iter (option_iter check_scope) scl;
+  List.iter (Option.iter check_scope) scl;
   arguments_scope := Refmap.add r scl !arguments_scope
 
 let cache_arguments_scope o =