Standardisation nom option_app en option_map

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 34 insertions, 34 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 57946eacc..425221675 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -429,7 +429,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_app 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
@@ -1167,7 +1167,7 @@ let rec generalize_problem pb current = function
       let tomatch = regeneralize_index_tomatch (i+1) tomatch in
       { pb with
 	  tomatch = Abstract d :: tomatch;
-          pred = option_app (generalize_predicate current i d) pb'.pred }
+          pred = option_map (generalize_predicate current i d) pb'.pred }
 
 (* No more patterns: typing the right-hand-side of equations *)
 let build_leaf pb =
@@ -1182,7 +1182,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_app (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 }
 
@@ -1252,7 +1252,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_app (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 }
 
@@ -1324,7 +1324,7 @@ and compile_generalization pb d rest =
     { pb with
        env = push_rel d pb.env;
        tomatch = rest;
-       pred = option_app ungeneralize_predicate pb.pred;
+       pred = option_map ungeneralize_predicate pb.pred;
        mat = List.map (push_rels_eqn [d]) pb.mat } in
   let patstat,j = compile pb in
   patstat, 
@@ -1350,7 +1350,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
     {pb with
        env = newenv;
        tomatch = tomatch;
-       pred = option_app (lift_predicate n) pb.pred;
+       pred = option_map (lift_predicate n) pb.pred;
        history = history;
        mat = mat } in
   let patstat,j = compile pb in
@@ -1538,7 +1538,7 @@ let extract_arity_signature env0 tomatchl tmsign =
     match tm with
       | NotInd (bo,typ) -> 
 	  (match t with
-	    | None -> [na,option_app (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"))
@@ -1610,7 +1610,7 @@ let prepare_predicate loc typing_fun isevars 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_app (fun tycon -> 
+	option_map (fun tycon -> 
 		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon)
 	  tycon
       in
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index d7c8a6dd0..b593411ea 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -84,10 +84,10 @@ let clenv_environments evd bound c =
 	  let dep = dependent (mkRel 1) c2 in
 	  let na' = if dep then na else Anonymous in
 	  let e' = meta_declare mv c1 ~name:na' e in
-	  clrec (e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
+	  clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) c2) else c2)
       | (n, LetIn (na,b,_,c)) ->
-	  clrec (e,metas) (option_app ((+) (-1)) n) (subst1 b c)
+	  clrec (e,metas) (option_map ((+) (-1)) n) (subst1 b c)
       | (n, _) -> (e, List.rev metas, c)
   in 
   clrec (evd,[]) bound c
@@ -100,10 +100,10 @@ let clenv_environments_evars env evd bound c =
       | (n, Prod (na,c1,c2)) ->
           let e',constr = Evarutil.new_evar e env c1 in
 	  let dep = dependent (mkRel 1) c2 in
-	  clrec (e', constr::ts) (option_app ((+) (-1)) n)
+	  clrec (e', constr::ts) (option_map ((+) (-1)) n)
 	    (if dep then (subst1 constr c2) else c2)
       | (n, LetIn (na,b,_,c)) ->
-	  clrec (e,ts) (option_app ((+) (-1)) n) (subst1 b c)
+	  clrec (e,ts) (option_map ((+) (-1)) n) (subst1 b c)
       | (n, _) -> (e, List.rev ts, c)
   in 
   clrec (evd,[]) bound c
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index aa4a200e7..1b128e43a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -168,7 +168,7 @@ module Default = 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_app (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' ->
@@ -184,7 +184,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_app (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 *)
@@ -201,7 +201,7 @@ module Default = struct
 			     let (evd'', v2', t2') = 
 			       let v2 =
 				 match v with 
-				     Some v -> option_app (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 
@@ -212,7 +212,7 @@ module Default = struct
 			       in
 				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
 			     in
-			       (evd'', option_app (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 6789459e8..25cf2aedd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -305,7 +305,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
     then 
       Anonymous, None, None
     else
-      match option_app 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
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2c5a0f901..9f4f1def1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -41,7 +41,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_app (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 0e3b8f62b..2785d0838 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -209,7 +209,7 @@ let push_rel_context_to_named_context env =
        let id = next_name_away na avoid in
        ((mkVar id)::subst,
         id::avoid,
-	push_named (id,option_app (substl subst) c,
+	push_named (id,option_map (substl subst) c,
                         type_app (substl subst) t)
 	  env))
     (rel_context env) ~init:([],ids_of_named_context (named_context env),env)
@@ -679,7 +679,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_app (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/pattern.ml b/pretyping/pattern.ml
index 9029578cd..5b3eafb30 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -152,7 +152,7 @@ let rec inst lvar = function
   | PProd (n,a,b) -> PProd (n,inst lvar a,inst lvar b)
   | PLetIn (n,a,b) -> PLetIn (n,inst lvar a,inst lvar b)
   | PCase (ci,po,p,pl) ->
-      PCase (ci,option_app (inst lvar) po,inst lvar p,Array.map (inst lvar) pl)
+      PCase (ci,option_map (inst lvar) po,inst lvar p,Array.map (inst lvar) pl)
   (* Non recursive *)
   | (PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ as x) -> x 
   (* Bound to terms *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index a0f69e701..19e86998f 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -59,7 +59,7 @@ let env_ise sigma env =
   Sign.fold_rel_context
     (fun (na,b,ty) e ->
       push_rel
-        (na, option_app (nf_evar sigma) b, nf_evar sigma ty)
+        (na, option_map (nf_evar sigma) b, nf_evar sigma ty)
         e)
     ctxt
     ~init:env0
@@ -75,7 +75,7 @@ let contract env lc =
 	  env
       | _ -> 
 	  let t' = substl !l t in
-	  let c' = option_app (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/pretyping.ml b/pretyping/pretyping.ml
index 64ea0bbb8..82a45ad44 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -385,7 +385,7 @@ module Pretyping_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_app 
+			option_map 
 			  (fun (abs, ty) ->
 			     match abs with
 				 None ->
@@ -401,7 +401,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
 			    uj_type = nf_isevar !isevars typ' }
-			  (option_app (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
@@ -409,7 +409,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = option_app (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
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 86ed95106..0fafb916d 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -96,7 +96,7 @@ let cases_predicate_names tml =
 
    - boolean in POldCase means it is recursive
 i*)
-let map_rawdecl f (na,obd,ty) = (na,option_app 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)
@@ -105,13 +105,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_app 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_app 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_app 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)
@@ -144,7 +144,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_app (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 b3180b06b..983f58f9c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -67,7 +67,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_app 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 10322c156..4e9a36f2e 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_app (lift n) v
+      option_map (lift n) v
   | EvalEvar ev -> Evd.existential_opt_value sigma ev
 
 exception NotEvaluable
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 597ddac57..faf91247e 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -961,7 +961,7 @@ let assums_of_rel_context sign =
 let lift_rel_context n sign =
   let rec liftrec k = function
     | (na,c,t)::sign ->
-	(na,option_app (liftn n k) c,type_app (liftn n k) t)
+	(na,option_map (liftn n k) c,type_app (liftn n k) t)
 	::(liftrec (k-1) sign)
     | [] -> []
   in