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

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.