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

5 files changed, 11 insertions, 11 deletions

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 6b14fd304..23c1028a4 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -216,7 +216,7 @@ let rec type_v_knsubst s = function
 and type_c_knsubst s ((id,v),e,pl,q) =
   ((id, type_v_knsubst s v), e, 
    List.map (fun p -> { p with p_value = subst_mps s p.p_value }) pl,
-   option_map (fun q -> { q with a_value = subst_mps s q.a_value }) q)
+   Option.map (fun q -> { q with a_value = subst_mps s q.a_value }) q)
 
 and binder_knsubst s (id,b) = 
   (id, match b with BindType v -> BindType (type_v_knsubst s v) | _ -> b)
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index 1a4ddbc2c..a341ba2ba 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -76,9 +76,9 @@ let rec abstract_post ren env (e,q) =
   let after_id id = id_of_string ((string_of_id id) ^ "'") in
   let (_,go) = Peffect.get_repr e in
   let al = List.map (fun id -> (id,after_id id)) go in
-  let q = option_map (named_app (subst_in_constr al)) q in
+  let q = Option.map (named_app (subst_in_constr al)) q in
   let tgo = List.map (fun (id,aid) -> (aid, trad_type_in_env ren env id)) al in
-  option_map (named_app (abstract tgo)) q
+  Option.map (named_app (abstract tgo)) q
 
 (* Translation of effects types in cic types.
  *
@@ -365,7 +365,7 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
 	    @(eq_phi ren'' env s svi tf)
 	    @(List.map (fun c -> CC_hole c) holes))
   in
-  let qapp' = option_map (named_app (subst_in_constr svi)) qapp in
+  let qapp' = Option.map (named_app (subst_in_constr svi)) qapp in
   let t = 
     make_let_in ren'' env fe [] (current_vars ren''' outf,qapp')
       (res,tyres) (t,ty)
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 72b609b24..bb9a355c3 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -787,7 +787,7 @@ END
 
 VERNAC COMMAND EXTEND Correctness
   [ "Correctness" preident(str) program(pgm) then_tac(tac) ]
-   -> [ Ptactic.correctness str pgm (option_map Tacinterp.interp tac) ]
+   -> [ Ptactic.correctness str pgm (Option.map Tacinterp.interp tac) ]
 END
 
 (* Show Programs *)
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 46cd12403..e4bac65f4 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -41,7 +41,7 @@ let anonymous x = { a_name = Anonymous; a_value = x }
 let anonymous_pre b x = { p_assert = b; p_name = Anonymous; p_value = x }
 
 let force_name f x =
-  option_map (fun q -> { a_name = Name (f q.a_name); a_value = q.a_value }) x
+  Option.map (fun q -> { a_name = Name (f q.a_name); a_value = q.a_value }) x
 
 let force_post_name x = force_name post_name x
 
@@ -143,7 +143,7 @@ let rec type_c_subst s ((id,t),e,p,q) =
   let s' = s @ List.map (fun (x,x') -> (at_id x "", at_id x' "")) s in
   (id, type_v_subst s t), Peffect.subst s e,
   List.map (pre_app (subst_in_constr s)) p,
-  option_map (post_app (subst_in_constr s')) q
+  Option.map (post_app (subst_in_constr s')) q
 
 and type_v_subst s = function
     Ref v -> Ref (type_v_subst s v)
@@ -160,7 +160,7 @@ and binder_subst s = function
 let rec type_c_rsubst s ((id,t),e,p,q) =
   (id, type_v_rsubst s t), e,
     List.map (pre_app (real_subst_in_constr s)) p,
-    option_map (post_app (real_subst_in_constr s)) q
+    Option.map (post_app (real_subst_in_constr s)) q
 
 and type_v_rsubst s = function
     Ref v -> Ref (type_v_rsubst s v)
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index 70e9eee29..258a46150 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -64,7 +64,7 @@ let update_post env top ef c =
 let force_post up env top q e =
   let (res,ef,p,_) = e.info.kappa in
   let q' = 
-    if up then option_map (named_app (update_post env top ef)) q else q 
+    if up then Option.map (named_app (update_post env top ef)) q else q 
   in
   let i = { env = e.info.env; kappa = (res,ef,p,q') } in
   { desc = e.desc; pre = e.pre; post = q'; loc = e.loc; info = i }
@@ -260,7 +260,7 @@ and propagate ren p =
     | Apply (f,l) ->
 	let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in
 	if ok then
-	  let q = option_map (named_app (real_subst_in_constr so)) qapp in
+	  let q = Option.map (named_app (real_subst_in_constr so)) qapp in
 	  post_if_none env q p
 	else
 	  p
@@ -285,7 +285,7 @@ and propagate ren p =
 	    None -> Some (anonymous s)
 	  | Some i -> Some { a_value = conj i.a_value s; a_name = i.a_name }
 	in
-	let q = option_map (named_app abstract_unit) q in
+	let q = Option.map (named_app abstract_unit) q in
 	post_if_none env q p
 
     | SApp ([Variable id], [e1;e2])