From 729b9a0a10eec0c67680b738ca52b4e85cb23f1b Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 13 Mar 2011 17:35:47 +0000 Subject: Fix inductive_template building ill-typed evars, and update test-suite scripts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13909 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/apply.v | 9 ++++----- test-suite/success/setoid_test.v | 2 +- 2 files changed, 5 insertions(+), 6 deletions(-) (limited to 'test-suite') 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. -- cgit v1.2.3