From 2ea625b086652cd77d09a52585dc7b4a5a263d76 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Nov 2002 21:40:30 +0000
Subject: Compatibilité avec les << >> dans la très ancienne syntaxe des actions
 de Grammar.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3240 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pcoq.ml4 | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 9c206565e6..6472dbaf5f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -482,7 +482,11 @@ let dynconstr = Gram.Entry.create "Constr.dynconstr"
 let dyncasespattern = Gram.Entry.create "Constr.dyncasespattern"
 
 GEXTEND Gram
-  dynconstr: [ [ a = Constr.constr -> ConstrNode a ] ];
+  dynconstr:
+  [ [ a = Constr.constr -> ConstrNode a 
+    (* For compatibility *)
+    | "<<"; a = Constr.constr; ">>" -> ConstrNode a ] ]
+  ;
   dyncasespattern: [ [ a = Constr.pattern -> CasesPatternNode a ] ];
 END
 
-- 
cgit v1.2.3