diff options
| author | clrenard | 2001-05-29 11:47:52 +0000 |
|---|---|---|
| committer | clrenard | 2001-05-29 11:47:52 +0000 |
| commit | 6a617ef747adf198caef983aead1c2e2c63c2afa (patch) | |
| tree | 36b04189cfdaa3dfbe8abe714dac98a052536e2c | |
| parent | b7c83140ffcfef871ac2d8eab342ec489f298c8a (diff) | |
Correction d'un bug du pretty-print
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1770 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Init/SpecifSyntax.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index bae1b2a1a6..1f4d0278e8 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -51,11 +51,12 @@ Syntax constr sig_var [<<(ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sig " $c1:L [1 1] $c2:L ] ] | sig2_var - [<<(Sig2_ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sig2 " $c1:L [1 1] $c2:L ] ] + [<<(Sig2_ABSTR_B_NB $c1 $c2 $c3)>>] + -> [ [<hov 0> "sig2 " $c1:L [1 1] $c2:L [1 1] $c3:L] ] | sigS_var [<<(SigS_ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sigS " $c1:L [1 1] $c2:L ] ] | sigS2_var [<<(SigS2_ABSTR_B_NB $c1 $c2 $c3)>>] - -> [ [<hov 0> "sigS2 " $c1:L [1 1] $c2:L [1 1] $c3:L] ] + -> [ [<hov 0> "sigS2 " $c1:L [1 1] $c2:L [1 1] $c3:L] ] ; level 1: |