From e14d23caa5810ec3e7c0d97c626d3dce997f79a6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 11 Jul 2002 19:17:27 +0000
Subject: Hack pour parser '{x:T|P}*B' sans parentheses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2857 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/SpecifSyntax.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 8d09ccd9bc..275bb80594 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -13,6 +13,23 @@ Require Specif.
 
 (** Parsing of things in Specif.v *)
 
+(* To accept {x:A|P}*B without parentheses *)
+Grammar constr constr3 :=
+  sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" "*" constr($c) ]
+       -> [ (prod (sig $c1 [$lc : $c1]$c2) $c) ]
+
+| sig2 [ "{" lconstr($lc) ":" lconstr($c1)
+           "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr($c) ]
+       -> [ (prod (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ]
+
+| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" "*" constr($c)]
+       -> [ (prod (sigS $c1 [$lc : $c1]$c2) $c) ]
+
+| sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
+             "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr($c) ]
+       -> [ (prod (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ].
+
+(* To factor with {A}+{B} *)
 Grammar constr constr3 :=
   sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
        -> [ (sig $c1 [$lc : $c1]$c2) ]
-- 
cgit v1.2.3