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

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 65976a03f9..24f5a78c5e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -387,7 +387,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try
     if !Flags.raw_print or !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
-    match availability_of_prim_token sc scopes with
+    match availability_of_prim_token p sc scopes with
     | None -> raise No_match
     | Some key ->
       let loc = cases_pattern_loc pat in
@@ -604,7 +604,7 @@ let rec rename_rawconstr_var id0 id1 = function
 let extern_possible_prim_token scopes r =
   try
     let (sc,n) = uninterp_prim_token r in
-    match availability_of_prim_token sc scopes with
+    match availability_of_prim_token n sc scopes with
     | None -> None
     | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
   with No_match ->
-- 
cgit v1.2.3