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

12 files changed, 33 insertions, 33 deletions

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 403ab8b9d6..6b14fd3048 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_app (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 5d1e55e3c3..1a4ddbc2c7 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_app (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_app (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_app (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 ece4668493..f6aad378d8 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -786,7 +786,7 @@ END
 
 VERNAC COMMAND EXTEND Correctness
   [ "Correctness" preident(str) program(pgm) then_tac(tac) ]
-   -> [ Ptactic.correctness str pgm (option_app 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 29064578f1..46cd124039 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_app (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_app (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_app (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 b7c6ac8c13..70e9eee293 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_app (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_app (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_app (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]) 
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 2b713c5149..1d1383f60f 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -401,7 +401,7 @@ let print_structure_to_file f prm struc =
     else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
   in
   (* print the implementation *)
-  let cout = option_app (fun (f,_) -> open_out f) f in 
+  let cout = option_map (fun (f,_) -> open_out f) f in 
   let ft = match cout with 
     | None -> !Pp_control.std_ft
     | Some cout -> Pp_control.with_output_to cout in 
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index e6f7b03cb2..451ac33d8c 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -83,14 +83,14 @@ let normalize_evaluables=
 
 TACTIC EXTEND firstorder
     [ "firstorder" tactic_opt(t) "with" ne_reference_list(l) ] -> 
-      [ gen_ground_tac true (option_app eval_tactic t) (Ids l) ]
+      [ gen_ground_tac true (option_map eval_tactic t) (Ids l) ]
 |   [ "firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> 
-      [ gen_ground_tac true (option_app eval_tactic t) (Bases l) ]
+      [ gen_ground_tac true (option_map eval_tactic t) (Bases l) ]
 |   [ "firstorder" tactic_opt(t) ] -> 
-      [ gen_ground_tac true (option_app eval_tactic t) Void ]
+      [ gen_ground_tac true (option_map eval_tactic t) Void ]
 END
 
 TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
-     [ gen_ground_tac false (option_app eval_tactic t) Void ]
+     [ gen_ground_tac false (option_map eval_tactic t) Void ]
 END
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index cd09fb5f29..f99aa86c8b 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -113,7 +113,7 @@ let change_vars =
       | RLetTuple(loc,nal,(na,rto),b,e) -> 
 	  RLetTuple(loc,
 		    nal, 
-		    (na, option_app (change_vars mapping) rto), 
+		    (na, option_map (change_vars mapping) rto), 
 		    change_vars mapping b,
 		    change_vars mapping e
 		   )
@@ -126,7 +126,7 @@ let change_vars =
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc,
 	      change_vars mapping b,
-	      (na,option_app (change_vars mapping) e_option),
+	      (na,option_map (change_vars mapping) e_option),
 	      change_vars mapping lhs,
 	      change_vars mapping rhs
 	     )
@@ -292,11 +292,11 @@ let rec alpha_rt excluded rt =
 	  if idmap_is_empty mapping
 	  then rto,t,b
 	  else let replace = change_vars mapping in 
-	  (option_app replace rto,replace t,replace b)
+	  (option_map replace rto,replace t,replace b)
 	in
 	let new_t = alpha_rt new_excluded new_t in 
 	let new_b = alpha_rt new_excluded new_b in 
-	let new_rto = option_app (alpha_rt new_excluded) new_rto  in
+	let new_rto = option_map (alpha_rt new_excluded) new_rto  in
 	RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
     | RCases(loc,infos,el,brl) -> 
 	let new_el = 
@@ -305,7 +305,7 @@ let rec alpha_rt excluded rt =
 	RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) 
     | RIf(loc,b,(na,e_o),lhs,rhs) -> 
 	RIf(loc,alpha_rt excluded b,
-	    (na,option_app (alpha_rt excluded) e_o),
+	    (na,option_map (alpha_rt excluded) e_o),
 	    alpha_rt excluded lhs,
 	    alpha_rt excluded rhs
 	   )
@@ -450,7 +450,7 @@ let replace_var_by_term x_id term =
       | RLetTuple(loc,nal,(na,rto),def,b) -> 
 	  RLetTuple(loc,
 		    nal,
-		    (na,option_app replace_var_by_pattern rto),
+		    (na,option_map replace_var_by_pattern rto),
 		    replace_var_by_pattern def,
 		    replace_var_by_pattern b
 		   )
@@ -462,7 +462,7 @@ let replace_var_by_term x_id term =
 		)
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc, replace_var_by_pattern b,
-	      (na,option_app replace_var_by_pattern e_option),
+	      (na,option_map replace_var_by_pattern e_option),
 	      replace_var_by_pattern lhs,
 	      replace_var_by_pattern rhs
 	     )
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index a78c35d1dd..21138c85e4 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1818,7 +1818,7 @@ let rec xlate_vernac =
 	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
            xlate_binder_list bl, xlate_formula c))
   | VernacSuspend -> CT_suspend
-  | VernacResume idopt -> CT_resume (xlate_ident_opt (option_app snd idopt))
+  | VernacResume idopt -> CT_resume (xlate_ident_opt (option_map snd idopt))
   | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND
 	(CT_theorem_goal
@@ -1860,7 +1860,7 @@ let rec xlate_vernac =
       (_, (add_coercion, (_,s)), binders, c1,
        rec_constructor_or_none, field_list) ->
       let record_constructor =
-        xlate_ident_opt (option_app snd rec_constructor_or_none) in
+        xlate_ident_opt (option_map snd rec_constructor_or_none) in
       CT_record
        ((if add_coercion then CT_coercion_atm else
           CT_coerce_NONE_to_COERCION_OPT(CT_none)),
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 5703c0efc1..437acb1f27 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -128,7 +128,7 @@ let eterm_term evm t tycon =
   let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in
     (* Generalize over the existential variables *)
   let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl 
-  and tycon = option_app 
+  and tycon = option_map 
 		(fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon
   in
   let _declare_evar (id, c) =
@@ -144,7 +144,7 @@ let eterm_term evm t tycon =
 	   Termops.print_constr_env (Global.env ()) t);
     trace (str "Term constructed in eterm" ++ spc () ++
 	   Termops.print_constr_env (Global.env ()) t'');
-    ignore(option_app 
+    ignore(option_map 
 	     (fun typ ->
 		trace (str "Type :" ++ spc () ++
 		       Termops.print_constr_env (Global.env ()) typ))
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index a138c69413..4a9cf8eb47 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -244,7 +244,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_app (app_opt coercion) v, t
+      !evars, option_map (app_opt coercion) v, t
 	
   (* Taken from pretyping/coercion.ml *)
 
@@ -371,7 +371,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_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' ->
@@ -387,7 +387,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_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 *)
@@ -404,7 +404,7 @@ module Coercion = 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 
@@ -415,7 +415,7 @@ module Coercion = 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/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 727ba82ae3..24edeba699 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -209,7 +209,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		let env', binders_rel = interp_context isevars env0 bl in
 		let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
 		let argid = match argname with Name n -> n | _ -> assert(false) in
-		let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in
+		let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in
 		let envwf = push_rel_context before env0 in
 		let wf_rel = interp_constr isevars envwf r in
 		let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in