diff options
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 9 | ||||
| -rw-r--r-- | test-suite/success/setoid_test.v | 2 |
3 files changed, 6 insertions, 7 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 5e2c0729c8..331cd01231 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 a6f9fa238d..d1efbca85a 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 63ca8aff4c..19693d70c9 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. |