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

3 files changed, 6 insertions, 7 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5e2c0729c..331cd0123 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -313,7 +313,7 @@ let inductive_template evdref env tmloc ind =
 	    let e = e_new_evar evdref env ~src:(hole_source n) ty' in
 	    (e::subst,e::evarl,n+1)
 	| Some b ->
-	    (b::subst,evarl,n+1))
+	    (substl subst b::subst,evarl,n+1))
       arsign ([],[],1) in
    applist (mkInd ind,List.rev evarl)
 
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.