diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/apply.v | 9 | ||||
| -rw-r--r-- | test-suite/success/setoid_test.v | 2 |
2 files changed, 5 insertions, 6 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. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 63ca8aff4..19693d70c 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -144,7 +144,7 @@ Section mult. Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). Proof. intros. setoid_rewrite fold_lemma. - change (fold A A (fun x0 : A, ab A x0) x = anat A (fold A nat (ab nat) x)). + change (fold A A (fun x0 : A => ab A x0) x = anat A (fold A nat (ab nat) x)). Abort. End mult. |