Creation of a new token PATTERNIDENT (?ident) for intro patterns, so

that "intros ? a ? b" behaves as expected.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10155 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 1 deletions

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index d2d5ad36a..8501b3436 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -27,13 +27,19 @@ GEXTEND Gram
   GLOBAL: 
     bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath
-    ne_string string;
+    ne_string string pattern_ident pattern_identref;
   preident:
     [ [ s = IDENT -> s ] ]
   ;
   ident:
     [ [ s = IDENT -> id_of_string s ] ]
   ;
+  pattern_ident:
+    [ [ s = PATTERNIDENT -> id_of_string s ] ]
+  ;
+  pattern_identref:
+    [ [ id = pattern_ident -> (loc, id) ] ]
+  ;
   var: (* as identref, but interpret as a term identifier in ltac *)
     [ [ id = ident -> (loc,id) ] ]
   ;