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

diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index e54c59058f..34c398289a 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -385,7 +385,7 @@ let mkDeclTomatch na = function
 
 let map_tomatch_type f = function
   | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind)
-  | NotInd (c,t) -> NotInd (option_map f c, f t)
+  | NotInd (c,t) -> NotInd (Option.map f c, f t)
 
 let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
 let lift_tomatch_type n = liftn_tomatch_type n 1
@@ -1127,7 +1127,7 @@ let rec generalize_problem pb = function
       let tomatch = regeneralize_index_tomatch (i+1) tomatch in
       { pb with
 	  tomatch = Abstract d :: tomatch;
-          pred = option_map (generalize_predicate i d) pb'.pred }
+          pred = Option.map (generalize_predicate i d) pb'.pred }
 
 (* No more patterns: typing the right-hand-side of equations *)
 let build_leaf pb =
@@ -1142,7 +1142,7 @@ let build_leaf pb =
 let shift_problem (current,t) pb =
   {pb with
      tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
-     pred = option_map (specialize_predicate_var (current,t)) pb.pred;
+     pred = Option.map (specialize_predicate_var (current,t)) pb.pred;
      history = push_history_pattern 0 AliasLeaf pb.history;
      mat = List.map remove_current_pattern pb.mat }
 
@@ -1207,7 +1207,7 @@ let build_branch current deps pb eqns const_info =
   let cur_alias = lift (List.length sign) current in
   let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in
   let env' = push_rels sign pb.env in
-  let pred' = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
+  let pred' = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
     sign,
   { pb with
       env = env';
@@ -1279,7 +1279,7 @@ and compile_generalization pb d rest =
     { pb with
        env = push_rel d pb.env;
        tomatch = rest;
-       pred = option_map ungeneralize_predicate pb.pred;
+       pred = Option.map ungeneralize_predicate pb.pred;
        mat = List.map (push_rels_eqn [d]) pb.mat } in
   let j = compile pb in
   { uj_val = mkLambda_or_LetIn d j.uj_val;
@@ -1304,7 +1304,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
     {pb with
        env = newenv;
        tomatch = tomatch;
-       pred = option_map (lift_predicate n) pb.pred;
+       pred = Option.map (lift_predicate n) pb.pred;
        history = history;
        mat = mat } in
   let j = compile pb in
@@ -1487,7 +1487,7 @@ let extract_arity_signature env0 tomatchl tmsign =
     match tm with
       | NotInd (bo,typ) -> 
 	  (match t with
-	    | None -> [na,option_map (lift n) bo,lift n typ]
+	    | None -> [na,Option.map (lift n) bo,lift n typ]
 	    | Some (loc,_,_,_) -> 
  	    user_err_loc (loc,"",
 	    str "Unexpected type annotation for a term of non inductive type"))
@@ -1765,14 +1765,14 @@ let subst_rel_context k ctx subst =
   let (_, ctx') =
     List.fold_right 
       (fun (n, b, t) (k, acc) ->
-	 (succ k, (n, option_map (substnl subst k) b, substnl subst k t) :: acc))
+	 (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc))
       ctx (k, [])
   in ctx'
 
 let lift_rel_contextn n k sign =
   let rec liftrec k = function
     | (na,c,t)::sign ->
-	(na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
+	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
     | [] -> []
   in
   liftrec (rel_context_length sign + k) sign
@@ -2065,7 +2065,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 let liftn_rel_context n k sign =  
   let rec liftrec k = function
     | (na,c,t)::sign ->
-	(na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
+	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
     | [] -> []
   in
     liftrec (k + rel_context_length sign) sign
@@ -2074,10 +2074,10 @@ let nf_evars_env evar_defs (env : env) : env =
   let nf t = nf_isevar evar_defs t in
   let env0 : env = reset_context env in 
   let f e (na, b, t) e' : env =
-    Environ.push_named (na, option_map nf b, nf t) e'
+    Environ.push_named (na, Option.map nf b, nf t) e'
   in
   let env' = Environ.fold_named_context f ~init:env0 env in
-    Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, option_map nf b, nf t) e')
+    Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
      ~init:env' env
       
 let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 1fb079fac6..17bbb65bdc 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -305,7 +305,7 @@ module Coercion = struct
   let coerce_itf loc env isevars v t c1 =
     let evars = ref isevars in
     let coercion = coerce loc env evars t c1 in
-      !evars, option_map (app_opt coercion) v, t
+      !evars, Option.map (app_opt coercion) v, t
 	
   (* Taken from pretyping/coercion.ml *)
 
@@ -439,7 +439,7 @@ module Coercion = struct
 	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
 	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
 		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
-		    let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
+		    let v' = Option.map (whd_betadeltaiota env (evars_of isevars)) v in
 		    let (evd',b) =
 		      match v' with 
 			  Some v' ->
@@ -455,7 +455,7 @@ module Coercion = struct
 			     let env1 = push_rel (x,None,v1) env in
 			     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
 						       (Some v2) t2 u2 in
-			       (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
+			       (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2', 
 				mkProd (x, v1, t2'))
 			 | None ->
 			     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
@@ -472,7 +472,7 @@ module Coercion = struct
 			     let (evd'', v2', t2') = 
 			       let v2 =
 				 match v with 
-				     Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
+				     Some v -> Option.map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
 				   | None -> None
 			       and evd', t2 =
 				 match v1' with 
@@ -483,7 +483,7 @@ module Coercion = struct
 			       in
 				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
 			     in
-			       (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
+			       (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2',
 				mkProd (name, u1, t2')))
 		| _ -> raise NoCoercion))
 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index d7d304279a..49eab5d29d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -159,7 +159,7 @@ let list_of_local_binders l =
 
 let lift_binders k n l =
   let rec aux n = function
-    | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+    | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl
     | [] -> []
   in aux n l
 
@@ -326,7 +326,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 
 let nf_evar_context isevars ctx = 
   List.map (fun (n, b, t) -> 
-    (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
+    (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
     
 let build_mutrec lnameargsardef boxed = 
   let sigma = Evd.empty and env = Global.env () in 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 769aff9dcf..5e7f025be1 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -58,7 +58,7 @@ let subst_deps obls deps t =
        let xobl = obls.(x) in
 	 debug 3 (str "Trying to get body of obligation " ++ int x);
        let oblb = 
-	 try out_some xobl.obl_body
+	 try Option.get xobl.obl_body
 	 with _ ->
 	   debug 3 (str "Couldn't get body of obligation " ++ int x);
 	   assert(false)
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index ab542feb20..0ed0632c65 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -290,7 +290,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
 		      let tycon = 
-			option_map 
+			Option.map 
 			  (fun (abs, ty) ->
 			     match abs with
 				 None ->
@@ -306,7 +306,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
 			    uj_type = nf_isevar !isevars typ' }
-			  (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
+			  (Option.map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
 
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
@@ -314,7 +314,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in
+	let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in
 	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
 	let resj =
 	  match kind_of_term resj.uj_val with