diff options
| -rw-r--r-- | theories/Init/SpecifSyntax.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index 1b78cd5229..0c8700ceb1 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -8,18 +8,18 @@ Require Export Specif. Grammar command command1 := sig [ "{" lcommand($lc) ":" lcommand($c1) "|" lcommand($c2) "}" ] - -> [<<(sig $c1 [$lc:$c1]$c2)>>] + -> [<<(sig $c1 [$lc : $c1]$c2)>>] | sig2 [ "{" lcommand($lc) ":" lcommand($c1) "|" lcommand($c2) "&" lcommand($c3) "}" ] - -> [<<(sig2 $c1 [$lc:$c1]$c2 [$lc:$c1]$c3)>>] + -> [<<(sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>] | sigS [ "{" lcommand($lc) ":" lcommand($c1) "&" lcommand($c2) "}" ] - -> [<<(sigS $c1 [$lc:$c1]$c2)>>] + -> [<<(sigS $c1 [$lc : $c1]$c2)>>] | sigS2 [ "{" lcommand($lc) ":" lcommand($c1) "&" lcommand($c2) "&" lcommand($c3) "}" ] - -> [<<(sigS2 $c1 [$lc:$c1]$c2 [$lc:$c1]$c3)>>] + -> [<<(sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>] | squash [ "{" lcommand($lc) "}" ] -> [(SQUASH $lc)]. |