diff options
| author | Hugo Herbelin | 2015-05-06 18:54:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-06 18:54:18 +0200 |
| commit | 32a9a4e3656e581af41c26f48f63ed1daec331d8 (patch) | |
| tree | 8d6418bf4ed13360fd737983a93482ee21c5b63f /test-suite | |
| parent | 5a0d3395cd972393eaa7859f47a738cc99ea55c6 (diff) | |
Fixing treatment of recursive equations damaged by 857e82b2ca0d1.
Improving treatment of recursive equations compared to 8.4 (see test-suite).
Experimenting not to unfold local defs ever in subst.
(+ Slight simplification in checking reflexive equalities only once).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/subst.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v new file mode 100644 index 0000000000..8336f6a806 --- /dev/null +++ b/test-suite/success/subst.v @@ -0,0 +1,25 @@ +(* Test various subtleties of the "subst" tactics *) + +(* Should proceed from left to right (see #4222) *) +Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y. +intros. +subst. +change (3 = 2) in H1. +change (3 = 3). +Abort. + +(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *) +Goal forall x y, x = y -> x = 3 -> x = y. +intros. +subst. +change (3 = 3). +Abort. + +(* Should substitute cycles once, until a recursive equation is obtained *) +(* (failed in 8.4) *) +Goal forall x y, x = S y -> y = S x -> x = y. +intros. +subst. +change (y = S (S y)) in H0. +change (S y = y). +Abort. |