diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/SpecifSyntax.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index 275bb8059..76ab4b3b9 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -15,18 +15,19 @@ Require Specif. (* To accept {x:A|P}*B without parentheses *) Grammar constr constr3 := - sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" "*" constr($c) ] + sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" "*" constr3($c) ] -> [ (prod (sig $c1 [$lc : $c1]$c2) $c) ] | sig2 [ "{" lconstr($lc) ":" lconstr($c1) - "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr($c) ] + "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ] -> [ (prod (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ] -| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" "*" constr($c)] +| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" + "*" constr3($c)] -> [ (prod (sigS $c1 [$lc : $c1]$c2) $c) ] | sigS2 [ "{" lconstr($lc) ":" lconstr($c1) - "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr($c) ] + "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ] -> [ (prod (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ]. (* To factor with {A}+{B} *) |