diff options
Diffstat (limited to 'test-suite/success/apply.v')
| -rw-r--r-- | test-suite/success/apply.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index a6f9fa238..d1efbca85 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -326,13 +326,12 @@ exact (refl_equal 4). Qed. (* From 12612, descent in conjunctions is more powerful *) -(* The following, which was failing badly in bug 1980, is now accepted - (even if somehow surprising) *) +(* The following, which was failing badly in bug 1980, is now + properly rejected, as descend in conjunctions builds an + ill-formed elimination from Prop to Type. *) Goal True. -eapply ex_intro. -instantiate (2:=fun _ :True => True). -instantiate (1:=I). +Fail eapply ex_intro. exact I. Qed. |