From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 parsing/g_prim.ml4 | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'parsing/g_prim.ml4')

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index d5ca5e0c..c3792d65 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -6,7 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: g_prim.ml4 7922 2006-01-23 19:11:11Z herbelin $ i*)
+(*i camlp4use: "pa_extend.cmo" i*)
+
+(*i $Id: g_prim.ml4 10155 2007-09-28 22:36:35Z glondu $ i*)
 
 open Pcoq
 open Names
@@ -25,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) ] ]
   ;
-- 
cgit v1.2.3