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

13 files changed, 40 insertions, 42 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fd8f24370a..058f3d210d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -421,7 +421,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
@@ -1139,7 +1139,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 =
@@ -1154,7 +1154,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 }
 
@@ -1224,7 +1224,7 @@ let build_branch current deps pb eqns const_info =
   { pb with
       env = push_rels sign pb.env;
       tomatch = List.rev_append currents tomatch;
-      pred = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
+      pred = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
       history = history;
       mat = List.map (push_rels_eqn_with_names sign) submat }
 
@@ -1291,7 +1291,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;
@@ -1316,7 +1316,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
@@ -1500,7 +1500,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"))
@@ -1566,7 +1566,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
       let allnames = List.rev (List.map (List.map pi1) arsign) in
       let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
       let _ = 
-	option_map (fun tycon -> 
+	Option.map (fun tycon -> 
 		      evdref := Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val 
 		      (lift_tycon_type (List.length arsign) tycon))
 	  tycon
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index dbc51514c1..b9881aaf04 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -106,7 +106,7 @@ let clenv_environments evd bound t =
 	  let dep = dependent (mkRel 1) t2 in
 	  let na' = if dep then na else Anonymous in
 	  let e' = meta_declare mv t1 ~name:na' e in
-	  clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n)
+	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) t2) else t2)
       | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
       | (n, _) -> (e, List.rev metas, t)
@@ -124,7 +124,7 @@ let clenv_environments_evars env evd bound t =
       | (n, Prod (na,t1,t2)) ->
           let e',constr = Evarutil.new_evar e env t1 in
 	  let dep = dependent (mkRel 1) t2 in
-	  clrec (e', constr::ts) (option_map ((+) (-1)) n)
+	  clrec (e', constr::ts) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 constr t2) else t2)
       | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t)
       | (n, _) -> (e, List.rev ts, t)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 62e29dc066..f3468bcbf1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -184,7 +184,7 @@ module Default = struct
       kind_of_term (whd_betadeltaiota env (evars_of evd) c1)
     with
     | Prod (_,t1,t2), Prod (name,u1,u2) -> 
-	let v' = option_map (whd_betadeltaiota env (evars_of evd)) v in
+	let v' = Option.map (whd_betadeltaiota env (evars_of evd)) v in
 	let (evd',b) =
 	  match v' with 
 	  | Some v' ->
@@ -201,7 +201,7 @@ module Default = 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 *)
@@ -219,7 +219,7 @@ module Default = struct
 	     let (evd'', v2', t2') = 
 	       let v2 =
 		 match v with 
-		 | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1'
+		 | Some v -> Option.map (fun x -> mkApp(lift 1 v,[|x|])) v1'
 		 | None -> None
 	       and evd', t2 =
 		 match v1' with 
@@ -231,7 +231,7 @@ module Default = 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/pretyping/detyping.ml b/pretyping/detyping.ml
index 829c5f4048..9dfe393bea 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -303,7 +303,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
     then 
       Anonymous, None, None
     else
-      match option_map detype p with
+      match Option.map detype p with
         | None -> Anonymous, None, None
         | Some p ->
             let nl,typ = it_destRLambda_or_LetIn_names k p in
@@ -340,7 +340,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 	array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in
       if array_for_all ((<>) None) nondepbrs then
 	RIf (dl,tomatch,(alias,pred),
-             out_some nondepbrs.(0),out_some nondepbrs.(1))
+             Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
 	RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
@@ -529,7 +529,7 @@ and detype_binder isgoal bk avoid env na ty c =
   | BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r)
 
 let rec detype_rel_context where avoid env sign =
-  let where = option_map (fun c -> it_mkLambda_or_LetIn c sign) where in
+  let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
   let rec aux avoid env = function
   | [] -> []
   | (na,b,t)::rest ->
@@ -539,7 +539,7 @@ let rec detype_rel_context where avoid env sign =
 	| Some c ->
 	    if b<>None then concrete_let_name None avoid env na c
 	    else concrete_name None avoid env na c in
-      let b = option_map (detype false avoid env) b in
+      let b = Option.map (detype false avoid env) b in
       let t = detype false avoid env t in
       (na',b,t) :: aux avoid' (add_name na' env) rest
   in aux avoid env (List.rev sign)
@@ -589,11 +589,11 @@ let rec subst_rawconstr subst raw =
 	  RLetIn (loc,n,r1',r2')
 
   | RCases (loc,rtno,rl,branches) -> 
-      let rtno' = option_smartmap (subst_rawconstr subst) rtno
+      let rtno' = Option.smartmap (subst_rawconstr subst) rtno
       and rl' = list_smartmap (fun (a,x as y) ->
         let a' = subst_rawconstr subst a in
         let (n,topt) = x in 
-        let topt' = option_smartmap
+        let topt' = Option.smartmap
           (fun (loc,(sp,i),x,y as t) ->
             let sp' = subst_kn subst sp in
             if sp == sp' then t else (loc,(sp',i),x,y)) topt in
@@ -611,14 +611,14 @@ let rec subst_rawconstr subst raw =
 	  RCases (loc,rtno',rl',branches')
 
   | RLetTuple (loc,nal,(na,po),b,c) ->
-      let po' = option_smartmap (subst_rawconstr subst) po
+      let po' = Option.smartmap (subst_rawconstr subst) po
       and b' = subst_rawconstr subst b 
       and c' = subst_rawconstr subst c in
 	if po' == po && b' == b && c' == c then raw else
           RLetTuple (loc,nal,(na,po'),b',c')
       
   | RIf (loc,c,(na,po),b1,b2) ->
-      let po' = option_smartmap (subst_rawconstr subst) po
+      let po' = Option.smartmap (subst_rawconstr subst) po
       and b1' = subst_rawconstr subst b1 
       and b2' = subst_rawconstr subst b2 
       and c' = subst_rawconstr subst c in
@@ -631,7 +631,7 @@ let rec subst_rawconstr subst raw =
       let bl' = array_smartmap
         (list_smartmap (fun (na,obd,ty as dcl) ->
           let ty' = subst_rawconstr subst ty in
-          let obd' = option_smartmap (subst_rawconstr subst) obd in
+          let obd' = Option.smartmap (subst_rawconstr subst) obd in
           if ty'==ty & obd'==obd then dcl else (na,obd',ty')))
         bl in
 	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9d0ae75e70..93e1c11576 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -43,7 +43,7 @@ let eval_flexible_term env c =
   match kind_of_term c with
   | Const c -> constant_opt_value env c
   | Rel n ->
-      (try let (_,v,_) = lookup_rel n env in option_map (lift n) v
+      (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v
       with Not_found -> None)
   | Var id ->
       (try let (_,v,_) = lookup_named id env in v with Not_found -> None)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index cb64fcb561..1f256b3bda 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -226,7 +226,7 @@ let push_rel_context_to_named_context env typ =
     Sign.fold_rel_context
       (fun (na,c,t) (subst, avoid, env) ->
 	let id = next_name_away na avoid in
-	let d = (id,option_map (substl subst) c,substl subst t) in
+	let d = (id,Option.map (substl subst) c,substl subst t) in
 	(mkVar id :: subst, id::avoid, push_named d env))
       (rel_context env) ~init:([], ids, env) in
   (named_context_val env, substl subst typ, inst_rels@inst_vars)
@@ -1133,7 +1133,7 @@ let lift_abstr_tycon_type n (abs, t) =
 	  else (Some (init, abs'), t)
 
 let lift_tycon_type n (abs, t) = (abs, lift n t)
-let lift_tycon n = option_map (lift_tycon_type n)
+let lift_tycon n = Option.map (lift_tycon_type n)
 
 let pr_tycon_type env (abs, t) =
   match abs with 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d0cbeb574c..6d75dada67 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -430,7 +430,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
     if filter = None then
       List.map (fun _ -> true) (named_context_of_val hyps)
     else
-      (let filter = out_some filter in
+      (let filter = Option.get filter in
       assert (List.length filter = List.length (named_context_of_val hyps));
       filter)
   in
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index cac06d2408..9ce8e703fe 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -153,7 +153,7 @@ let matches_core convert allow_partial_app pat c =
 	  sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2
 
       | PRef (ConstRef _ as ref), _ when convert <> None ->
-	  let (env,evars) = out_some convert in
+	  let (env,evars) = Option.get convert in
 	  let c = constr_of_global ref in
 	  if is_conv env evars c cT then sigma
 	  else raise PatternMatchingFailure
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index c3b49b9749..d64e84fea0 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -185,7 +185,7 @@ let rec subst_pattern subst pat = match pat with
 	if c' == c && c1' == c1 && c2' == c2 then pat else
 	  PIf (c',c1',c2')
   | PCase ((a,b,ind,n as cs),typ,c,branches) ->
-      let ind' = option_smartmap (Inductiveops.subst_inductive subst) ind in
+      let ind' = Option.smartmap (Inductiveops.subst_inductive subst) ind in
       let typ' = subst_pattern subst typ in 
       let c' = subst_pattern subst c in
       let branches' = array_smartmap (subst_pattern subst) branches in
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 26ccc8024b..ad4e06a55a 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -60,7 +60,7 @@ let env_ise sigma env =
   Sign.fold_rel_context
     (fun (na,b,ty) e ->
       push_rel
-        (na, option_map (nf_evar sigma) b, nf_evar sigma ty)
+        (na, Option.map (nf_evar sigma) b, nf_evar sigma ty)
         e)
     ctxt
     ~init:env0
@@ -76,7 +76,7 @@ let contract env lc =
 	  env
       | _ -> 
 	  let t' = substl !l t in
-	  let c' = option_map (substl !l) c in
+	  let c' = Option.map (substl !l) c in
 	  let na' = named_hd env t' na in
 	  l := (mkRel 1) :: List.map (lift 1) !l;
 	  push_rel (na',c',t') env in
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 63e40a0521..d2a3473632 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -101,7 +101,7 @@ let cases_predicate_names tml =
 
    - boolean in POldCase means it is recursive
 i*)
-let map_rawdecl f (na,obd,ty) = (na,option_map f obd,f ty)
+let map_rawdecl f (na,obd,ty) = (na,Option.map f obd,f ty)
 
 let map_rawconstr f = function
   | RVar (loc,id) -> RVar (loc,id)
@@ -110,13 +110,13 @@ let map_rawconstr f = function
   | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
   | RCases (loc,rtntypopt,tml,pl) ->
-      RCases (loc,option_map f rtntypopt,
+      RCases (loc,Option.map f rtntypopt,
         List.map (fun (tm,x) -> (f tm,x)) tml,
         List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
-      RLetTuple (loc,nal,(na,option_map f po),f b,f c)
+      RLetTuple (loc,nal,(na,Option.map f po),f b,f c)
   | RIf (loc,c,(na,po),b1,b2) ->
-      RIf (loc,f c,(na,option_map f po),f b1,f b2)
+      RIf (loc,f c,(na,Option.map f po),f b1,f b2)
   | RRec (loc,fk,idl,bl,tyl,bv) ->
       RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
             Array.map f tyl,Array.map f bv)
@@ -149,7 +149,7 @@ let map_rawconstr_with_binders_loc loc g f e = function
       let g' id e = snd (g id e) in
       let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
       RCases
-	(loc,option_map (f e) tyopt,List.map (f e) tml, List.map h pl)
+	(loc,Option.map (f e) tyopt,List.map (f e) tml, List.map h pl)
   | RRec (_,fk,idl,tyl,bv) ->
       let idl',e' = fold_ident g idl e in
       RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 8ca06e9a5f..4b93388d6e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -40,15 +40,13 @@ type struc_typ = {
 let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
 let projection_table = ref Cmap.empty
 
-let option_fold_right f p e = match p with Some a -> f a e | None -> e
-
 let load_structure i (_,(ind,id,kl,projs)) =
   let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
   let struc =
     { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
   structure_table := Indmap.add ind struc !structure_table;
   projection_table := 
-    List.fold_right (option_fold_right (fun proj -> Cmap.add proj struc))
+    List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc))
       projs !projection_table
 
 let cache_structure o =
@@ -60,7 +58,7 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
    list_smartmap 
-     (option_smartmap (fun kn -> fst (subst_con subst kn)))
+     (Option.smartmap (fun kn -> fst (subst_con subst kn)))
     projs
   in
     if projs' == projs && kn' == kn then obj else
@@ -68,7 +66,7 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
 
 let discharge_structure (_,(ind,id,kl,projs)) =
   Some (Lib.discharge_inductive ind, id, kl,
-        List.map (option_map Lib.discharge_con) projs)
+        List.map (Option.map Lib.discharge_con) projs)
 
 let (inStruc,outStruc) =
   declare_object {(default_object "STRUCTURE") with 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index bb89756b30..c4c9894cb4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -80,7 +80,7 @@ let reference_opt_value sigma env = function
       v
   | EvalRel n ->
       let (_,v,_) = lookup_rel n env in
-      option_map (lift n) v
+      Option.map (lift n) v
   | EvalEvar ev -> Evd.existential_opt_value sigma ev
 
 exception NotEvaluable