diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-03 15:00:32 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-03 15:27:04 +0100 |
| commit | 7af811e5100839484cbed0126b5c37a972487ec3 (patch) | |
| tree | 4a377904b91723805366bfc89bdcf2954037cbe5 /test-suite/success | |
| parent | 7d01d46ce0f9267446b474755762db1ccca5fd78 (diff) | |
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).
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/destruct.v | 10 |
1 files changed, 9 insertions, 1 deletions
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. |