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

1 files changed, 17 insertions, 0 deletions

diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 8d09ccd9b..275bb8059 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) ]