diff options
| -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 b0e8bd5ba4..50bed88279 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)>>]. |