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) ] ]
   ;