diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-10 17:49:33 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-10 17:49:33 +0000 |
| commit | cd3be69adce23c812c968ed33ecb6ea8b43ef2ab (patch) | |
| tree | d53e82a6cca456cd539e04df7d11f718b190ab83 /theories/Init/LogicSyntax.v | |
| parent | 6bae2b22d2280bf25685f8bea5e94fe766d136fa (diff) | |
t -> $t dans regle grammaire EX
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@313 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/LogicSyntax.v')
| -rw-r--r-- | theories/Init/LogicSyntax.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index b0e8bd5ba..50bed8827 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -42,7 +42,7 @@ with constr10 := | eximplicit [ "EX" ident($v) "|" constr($c1) ] -> [<<(ex ? [$v]$c1)>>] | ex2explicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) "&" - constr($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : t]$c2)>>] + constr($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : $t]$c2)>>] | ex2implicit [ "EX" ident($v) "|" constr($c1) "&" constr($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>]. |