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

2 files changed, 10 insertions, 10 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 207d78b193..82fbe9c691 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -187,7 +187,7 @@ and e_my_find_search db_list local_db hdc concl =
 		 (e_trivial_fail_db db_list local_db)
 	   | Unfold_nth c -> unfold_in_concl [[],c]
 	   | Extern tacast -> Auto.conclPattern concl 
-	       (out_some p) tacast
+	       (Option.get p) tacast
        in 
        (free_try tac,fmt_autotactic t))
        (*i
@@ -400,7 +400,7 @@ and my_find_search db_list local_db hdc concl =
 		(trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> unfold_in_concl [[],c]
 	  | Extern tacast -> 
-	      conclPattern concl (out_some p) tacast))
+	      conclPattern concl (Option.get p) tacast))
     tacl
 
 and trivial_resolve db_list local_db cl = 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 150b070f88..0e4f660724 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -306,7 +306,7 @@ let make_fix_struct (n,bl) =
   let nn = List.length names in
   if nn = 1 || n = None then ctv_ID_OPT_NONE
   else 
-    let n = out_some n in 
+    let n = Option.get n in 
     if n < nn then xlate_id_opt(List.nth names n)
     else xlate_error "unexpected result of parsing for Fixpoint";;
 
@@ -429,7 +429,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
 	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
          if bl = [] then
-	   let n = out_some n in 
+	   let n = Option.get n in 
            let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
            (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
          else (make_fix_struct (n, bl),bl,arf,ardef) in
@@ -995,7 +995,7 @@ and xlate_tac =
 	  let cl_as_xlate_arg = 
 	    {cl_as_clause with 
 	       Tacexpr.onhyps = 
-		option_map 
+		Option.map 
 		  (fun l -> 
 		     List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l
 		  )
@@ -1312,7 +1312,7 @@ and coerce_genarg_to_TARG x =
 					 (snd (out_gen
 					    (rawwit_open_constr_gen b) x))))
   | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
-      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let n = Option.get (Pcoq.tactic_genarg_level s) in
       let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_COM_to_TARG t
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
@@ -1405,7 +1405,7 @@ let coerce_genarg_to_VARG x =
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
   | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
-      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let n = Option.get (Pcoq.tactic_genarg_level s) in
       let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
   | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
@@ -1857,7 +1857,7 @@ let rec xlate_vernac =
 	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
            xlate_binder_list bl, xlate_formula c))
   | VernacSuspend -> CT_suspend
-  | VernacResume idopt -> CT_resume (xlate_ident_opt (option_map snd idopt))
+  | VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt))
   | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND
 	(CT_theorem_goal
@@ -1900,7 +1900,7 @@ let rec xlate_vernac =
       (_, (add_coercion, (_,s)), binders, c1,
        rec_constructor_or_none, field_list) ->
       let record_constructor =
-        xlate_ident_opt (option_map snd rec_constructor_or_none) in
+        xlate_ident_opt (Option.map snd rec_constructor_or_none) in
       CT_record
        ((if add_coercion then CT_coercion_atm else
           CT_coerce_NONE_to_COERCION_OPT(CT_none)),
@@ -1923,7 +1923,7 @@ let rec xlate_vernac =
 	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
 	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
          if bl = [] then
-	   let n = out_some n in 
+	   let n = Option.get n in 
            let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
            (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
          else (make_fix_struct (n, bl),bl,arf,ardef) in