From 7af811e5100839484cbed0126b5c37a972487ec3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 3 Nov 2014 15:00:32 +0100 Subject: Fix to 844431761 on improving elimination with indices, getting rid of intrusive residual local definitions + more conservative strategy for which variables are not generalized (point 2 of 4df1ddc6d6bd07073). --- test-suite/success/destruct.v | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'test-suite/success') diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index cca54bf1c..0faaa275f 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -341,7 +341,7 @@ Abort. Goal forall x y e (t:x=y) (z:x=y -> IND y x e), e = e. intros. destruct (z t). -change (x=y) in t. (* Generalization not made *) +change (0=0) in t. (* Generalization made *) Abort. Goal forall x y e (t:x=y) (z:x=y -> IND y x e), e = e /\ z t = z t. @@ -361,3 +361,11 @@ Goal (forall P:Prop, (nat->nat) -> P) -> forall h:nat->nat->nat, h 0 0 = h 1 0. intros. induction (h 1) using H. Qed. + +(* Check blocking generalization is not too strong (failed at some time) *) + +Goal (E -> 0=1) -> 1=0 -> True. +intros. +destruct (H _). +change (0=0) in H0. (* Check generalization on H0 was made *) +Abort. -- cgit v1.2.3