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

6 files changed, 7 insertions, 7 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 336f741aec..f7127ea616 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -160,7 +160,7 @@ type grammar_tactic_production =
 
 let make_prod_item = function
   | TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
-  | TacNonTerm (_,(nont,t), po) -> (nont, option_app (fun p -> (p,t)) po)
+  | TacNonTerm (_,(nont,t), po) -> (nont, option_map (fun p -> (p,t)) po)
 
 (* Tactic grammar extensions *)
 
@@ -232,7 +232,7 @@ let make_vprod_item n univ = function
   | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
   | VNonTerm (loc, nt, po) ->
       let (etyp, e) = interp_entry_name n univ nt in
-      e, option_app (fun p -> (p,etyp)) po
+      e, option_map (fun p -> (p,etyp)) po
 
 let get_tactic_entry n =
   if n = 0 then
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml
index e6324e0080..ac54fc63d5 100644
--- a/parsing/g_ascii_syntax.ml
+++ b/parsing/g_ascii_syntax.ml
@@ -72,7 +72,7 @@ let make_ascii_string n =
   if n>=32 && n<=126 then String.make 1 (char_of_int n)
   else Printf.sprintf "%03d" n
 
-let uninterp_ascii_string r = option_app make_ascii_string (uninterp_ascii r)
+let uninterp_ascii_string r = option_map make_ascii_string (uninterp_ascii r)
 
 let _ =
   Notation.declare_string_interpreter "char_scope"
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ed9e1fa06d..64d96ae4b6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -75,7 +75,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   (snd id,(n,ro),bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
-  let _ = option_app (fun (aloc,_) ->
+  let _ = option_map (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofixb",
        Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e8829acbab..5c847f5a48 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -102,7 +102,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
   (id,n,CProdN(loc,bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
-  let _ = option_app (fun (aloc,_) ->
+  let _ = option_map (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofix_tac",
        Pp.str"Annotation forbidden in cofix expression")) ann in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0a0df6fb21..94df46be84 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -429,7 +429,7 @@ GEXTEND Gram
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
          pos = OPT [ "["; l = LIST0 ident; "]" -> l ] ->
-	   let pos = option_app (List.map (fun id -> ExplByName id)) pos in
+	   let pos = option_map (List.map (fun id -> ExplByName id)) pos in
 	   VernacDeclareImplicits (qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 8d99ac1121..593595a230 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -401,7 +401,7 @@ let print_context with_values =
     | h::rest when n = None or out_some n > 0 -> 
 	(match print_library_entry with_values h with
 	  | None -> prec n rest
-	  | Some pp -> prec (option_app ((+) (-1)) n) rest ++ pp ++ fnl ())
+	  | Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ())
     | _ -> mt ()
   in 
   prec