diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-14 12:54:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-14 13:17:20 +0100 |
| commit | 194ad253a24ce542d9b1bb4c13ad0d2f64a0aa48 (patch) | |
| tree | 99f09e19a060d0f6bc812265221b2046aa7012ba /test-suite/success/induct.v | |
| parent | 1414ab30f9d030a4421da766121accb03276d827 (diff) | |
Preserving the good effect of 014e5ac92a on not leaving dangling local
definitions while keeping some compatibility on when to generalize
when an index also occur in a parameter (effect on PersistentUnionFind
for instance).
Diffstat (limited to 'test-suite/success/induct.v')
| -rw-r--r-- | test-suite/success/induct.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 0d0466cb5..3715f65f6 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -140,3 +140,14 @@ intros x H1 H. induction H. change True in IHrepr'. Abort. + +(* In this case, generalization was done in 8.4 and we preserve it; this + is arbitrary choice *) + +Inductive repr'' : nat -> nat -> Prop := reprc'' x z : repr'' x z -> repr'' x z. + +Goal forall x, 0 = x -> repr'' x x -> True. +intros x H1 H. +induction H. +change (0 = z -> True) in IHrepr''. +Abort. |