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

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index b10aa782c..45976d6e5 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -882,7 +882,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let f_def = Global.lookup_constant (destConst f) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
   let f_body =
-    force (out_some f_def.const_body)
+    force (Option.get f_def.const_body)
   in
   let params,f_body_with_params = decompose_lam_n nb_params f_body in
   let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -933,8 +933,8 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
   let equation_lemma = 
     try 
       let finfos = find_Function_infos (destConst f) in 
-      mkConst (out_some finfos.equation_lemma)
-    with (Not_found | Failure "out_some" as e) -> 
+      mkConst (Option.get finfos.equation_lemma)
+    with (Not_found | Option.IsNone as e) -> 
       let f_id = id_of_label (con_label (destConst f)) in 
       (*i The next call to mk_equation_id is valid since we will construct the lemma
 	Ensures by: obvious
@@ -943,7 +943,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
       generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
       let _ =
 	match e with 
-	  | Failure "out_some" -> 
+	  | Option.IsNone -> 
 	      let finfos = find_Function_infos (destConst f) in 
 	      update_Function 
 		{finfos with