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

diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index ec8a38501b..771dbe7363 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -25,10 +25,10 @@ open Pp
 let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) 
 
 let intern_justification_items globs = 
-  option_map (List.map (intern_constr globs))
+  Option.map (List.map (intern_constr globs))
 
 let intern_justification_method globs = 
-  option_map (intern_tactic globs)
+  Option.map (intern_tactic globs)
 
 let intern_statement intern_it globs st =
   {st_label=st.st_label;
@@ -52,7 +52,7 @@ let add_name nam globs=
 
 let intern_hyp iconstr globs = function 
     Hvar (loc,(id,topt)) -> add_var id globs,
-      Hvar (loc,(id,option_map (intern_constr globs) topt))
+      Hvar (loc,(id,Option.map (intern_constr globs) topt))
   | Hprop st -> add_name st.st_label globs,
       Hprop (intern_statement iconstr globs st)
 
@@ -73,7 +73,7 @@ let intern_casee globs = function
 let intern_hyp_list args globs =
   let intern_one globs (loc,(id,opttyp)) =
     (add_var id globs),
-    (loc,(id,option_map (intern_constr globs) opttyp)) in
+    (loc,(id,Option.map (intern_constr globs) opttyp)) in
   list_fold_map intern_one globs args 
 
 let intern_suffices_clause globs (hyps,c) = 
@@ -141,7 +141,7 @@ let rec intern_proof_instr globs instr=
 (* INTERP *)
 
 let interp_justification_items sigma env =
-    option_map (List.map (fun c ->understand sigma env (fst c)))
+    Option.map (List.map (fun c ->understand sigma env (fst c)))
 
 let interp_constr check_sort sigma env c = 
   if check_sort then