diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-15 14:16:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-15 14:16:14 +0000 |
| commit | 0b51e0bdc5c8953b79bc03796eba3738553b2f8e (patch) | |
| tree | b8b4434c3ce98b7075043bbe9f953030460a12db /theories | |
| parent | 4175a85ce18f047bdfc90b42205fa3c3d9895635 (diff) | |
Bug de précédence
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2869 85f007b7-540e-0410-9357-904b9bb8a0f7
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} *) |