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.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index bee6c5c931..794169a377 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -190,14 +190,14 @@ let prim_token_key_table = Hashtbl.create 7
 
 
 let make_gr = function
-  | ConstRef con -> 
+  | ConstRef con ->
       ConstRef(constant_of_kn(canonical_con con))
   | IndRef (kn,i) ->
       IndRef(mind_of_kn(canonical_mind kn),i)
   | ConstructRef ((kn,i),j )->
       ConstructRef((mind_of_kn(canonical_mind kn),i),j)
   | VarRef id ->  VarRef id
-      
+
 let rawconstr_key = function
   | RApp (_,RRef (_,ref),_) -> RefKey (make_gr ref)
   | RRef (_,ref) -> RefKey (make_gr ref)
@@ -409,8 +409,10 @@ let uninterp_prim_token_cases_pattern c =
       | Some n -> (na,sc,n)
   with Not_found -> raise No_match
 
-let availability_of_prim_token printer_scope local_scopes =
-  let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
+let availability_of_prim_token n printer_scope local_scopes =
+  let f scope =
+    try ignore (Hashtbl.find prim_token_interpreter_tab scope dummy_loc n); true
+    with Not_found -> false in
   let scopes = make_current_scopes local_scopes in
   Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
-- 
cgit v1.2.3