From 5ae3e803d6d8169deadef604fbc44fa86c13f876 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 10 Apr 2010 19:13:17 +0000
Subject: Optimized need for delimiters when disjoint scopes for strings and
 numerals are open (see e.g. part of bug report #2044).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12924 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index d549bb3878..f52e17cc86 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -98,7 +98,7 @@ val uninterp_prim_token_cases_pattern :
   cases_pattern -> name * scope_name * prim_token
 
 val availability_of_prim_token :
-  scope_name -> local_scopes -> delimiters option option
+  prim_token -> scope_name -> local_scopes -> delimiters option option
 
 (*s Declare and interpret back and forth a notation *)
 
-- 
cgit v1.2.3