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

8 files changed, 18 insertions, 18 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index e9200cd75a..cc5beb974e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -113,7 +113,7 @@ type recipe = {
   d_modlist : work_list }
 
 let on_body f = 
-  option_map (fun c -> Declarations.from_val (f (Declarations.force c)))
+  Option.map (fun c -> Declarations.from_val (f (Declarations.force c)))
 
 let cook_constant env r =
   let cb = r.d_from in
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index eb49ba6203..4a5893de8b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -56,7 +56,7 @@ type constant_body = {
     information). *)
 
 let subst_rel_declaration sub (id,copt,t as x) =
-  let copt' = option_smartmap (subst_mps sub) copt in
+  let copt' = Option.smartmap (subst_mps sub) copt in
   let t' = subst_mps sub t in
   if copt == copt' & t == t' then x else (id,copt',t')
 
@@ -198,7 +198,7 @@ let subst_arity sub = function
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 let subst_const_body sub cb = {
     const_hyps = (assert (cb.const_hyps=[]); []);
-    const_body = option_map (subst_constr_subst sub) cb.const_body;
+    const_body = Option.map (subst_constr_subst sub) cb.const_body;
     const_type = subst_arity sub cb.const_type;
     const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
     (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
@@ -241,7 +241,7 @@ let subst_mind sub mib =
       map_rel_context (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_constraints = mib.mind_constraints ;
-    mind_equiv = option_map (subst_kn sub) mib.mind_equiv }
+    mind_equiv = Option.map (subst_kn sub) mib.mind_equiv }
 
 
 (*s Modules: signature component specifications, module types, and
diff --git a/kernel/environ.ml b/kernel/environ.ml
index faf0757127..c2ec6ea7e0 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -89,7 +89,7 @@ let named_context_of_val = fst
    *** /!\ ***   [f t] should be convertible with t *)  
 let map_named_val f (ctxt,ctxtv) = 
   let ctxt =
-    List.map (fun (id,body,typ) -> (id, option_map f body, f typ)) ctxt in
+    List.map (fun (id,body,typ) -> (id, Option.map f body, f typ)) ctxt in
   (ctxt,ctxtv)
 
 let empty_named_context = empty_named_context 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 8770afe131..135a377471 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -163,7 +163,7 @@ and subst_module  sub mb =
      a module M in a signature that is knows to be equivalent to a module M'
      (because the signature is "K with Module M := M'") and we are substituting
      M' with some M''. *)
-  let mpo' = option_smartmap (subst_mp sub) mb.msb_equiv in
+  let mpo' = Option.smartmap (subst_mp sub) mb.msb_equiv in
     if mtb'==mb.msb_modtype && mpo'==mb.msb_equiv then mb else
       { msb_modtype=mtb'; 
 	msb_equiv=mpo'; 
@@ -274,7 +274,7 @@ let resolver_of_environment mbid modtype mp env =
 	   if expecteddef.Declarations.const_inline then
 	     let constant = lookup_constant con' env in
 	     if (not constant.Declarations.const_opaque) then
-	       let constr = option_map Declarations.force
+	       let constr = Option.map Declarations.force
 		 constant.Declarations.const_body in
 		 (con,constr)::(make_resolve r)
 	     else make_resolve r
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 91e4c73fc9..f7f6a980d3 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -329,7 +329,7 @@ let start_module l senv =
 let end_module l restype senv = 
   let oldsenv = senv.old in
   let modinfo = senv.modinfo in
-  let restype = option_map (translate_modtype senv.env) restype in
+  let restype = Option.map (translate_modtype senv.env) restype in
   let params = 
     match modinfo.variant with
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
@@ -633,9 +633,9 @@ let import (dp,mb,depends,engmt) digest senv =
  
 let rec lighten_module mb =
   { mb with
-    mod_expr = option_map lighten_modexpr mb.mod_expr;
+    mod_expr = Option.map lighten_modexpr mb.mod_expr;
     mod_type = lighten_modtype mb.mod_type;
-    mod_user_type = option_map lighten_modtype mb.mod_user_type }
+    mod_user_type = Option.map lighten_modtype mb.mod_user_type }
 
 and lighten_modtype = function
   | MTBident kn as x -> x
diff --git a/kernel/sign.ml b/kernel/sign.ml
index c2b4eca750..79619b48f1 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -73,7 +73,7 @@ let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
 
 let map_context f l =
   let map_decl (n, body_o, typ as decl) =
-    let body_o' = option_smartmap f body_o in
+    let body_o' = Option.smartmap f body_o in
     let typ' = f typ in
       if body_o' == body_o && typ' == typ then decl else
 	(n, body_o', typ')
@@ -83,8 +83,8 @@ let map_context f l =
 let map_rel_context = map_context
 let map_named_context = map_context
 
-let iter_rel_context f = List.iter (fun (_,b,t) -> f t; option_iter f b)
-let iter_named_context f = List.iter (fun (_,b,t) -> f t; option_iter f b)
+let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
 
 (* Push named declarations on top of a rel context *)
 (* Bizarre. Should be avoided. *)
@@ -92,7 +92,7 @@ let push_named_to_rel_context hyps ctxt =
   let rec push = function
     | (id,b,t) :: l ->
 	let s, hyps = push l in
-	let d = (Name id, option_map (subst_vars s) b, subst_vars s t) in
+	let d = (Name id, Option.map (subst_vars s) b, subst_vars s t) in
 	id::s, d::hyps
     | [] -> [],[] in
   let s, hyps = push hyps in
diff --git a/kernel/term.ml b/kernel/term.ml
index 4b01ac1cfe..b09bd4aea7 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -639,10 +639,10 @@ type strategy = types option
 type named_declaration = identifier * constr option * types
 type rel_declaration = name * constr option * types
 
-let map_named_declaration f (id, v, ty) = (id, option_map f v, f ty)
+let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty)
 let map_rel_declaration = map_named_declaration
 
-let fold_named_declaration f (_, v, ty) a = f ty (option_fold_right f v a)
+let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
 let fold_rel_declaration = fold_named_declaration
 
 (****************************************************************************)
@@ -773,7 +773,7 @@ let substl laml = substnl laml 0
 let subst1 lam = substl [lam]
 
 let substnl_decl laml k (id,bodyopt,typ) =
-  (id,option_map (substnl laml k) bodyopt,substnl laml k typ)
+  (id,Option.map (substnl laml k) bodyopt,substnl laml k typ)
 let substl_decl laml = substnl_decl laml 0
 let subst1_decl lam = substl_decl [lam]
 let subst1_named_decl = subst1_decl
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fd916e77b0..7a7e0bb5a0 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -470,7 +470,7 @@ let is_direct_sort_constraint s v = match s with
 
 let solve_constraints_system levels level_bounds =
   let levels = 
-    Array.map (option_map (function Atom u -> u | _ -> anomaly "expects Atom"))
+    Array.map (Option.map (function Atom u -> u | _ -> anomaly "expects Atom"))
       levels in
   let v = Array.copy level_bounds in
   let nind = Array.length v in