From 61d11c649b4cd68e92861e2fea86f6c6a6b5bb6a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 27 Apr 2006 19:37:33 +0000
Subject: 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
---
 interp/notation.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index d068cf64cc..74263b7683 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -234,12 +234,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x))
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
-    (patl, (fun r -> option_app mkNumeral (uninterp r)), inpat)
+    (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
-    (patl, (fun r -> option_app mkString (uninterp r)), inpat)
+    (patl, (fun r -> option_map mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.absolute_reference sp in ()
@@ -389,7 +389,7 @@ let uninterp_prim_token_cases_pattern c =
 
 let availability_of_prim_token printer_scope scopes =
   let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
-  option_app snd (find_without_delimiters f (Some printer_scope,None) scopes)
+  option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
 (* Miscellaneous *)
 
-- 
cgit v1.2.3