diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-30 18:59:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-02 20:44:14 +0200 |
| commit | 24d5448c65ba05072a5ab4180c9be95670ce126d (patch) | |
| tree | 855c71e8f733e7b23b5aef7ef226873704fa4d34 /test-suite/success/subst.v | |
| parent | decdd5b3cc322936f7d1e7cc3bb363a2957d404e (diff) | |
More tests for tactic "subst".
Diffstat (limited to 'test-suite/success/subst.v')
| -rw-r--r-- | test-suite/success/subst.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v index 8336f6a80..25ee81b58 100644 --- a/test-suite/success/subst.v +++ b/test-suite/success/subst.v @@ -23,3 +23,20 @@ subst. change (y = S (S y)) in H0. change (S y = y). Abort. + +(* A bug revealed by OCaml 4.03 warnings *) +(* fixes in 4e3d464 and 89ec88f for v8.5, 4e3d4646 and 89ec88f1e for v8.6 *) +Goal forall y, let x:=0 in y=x -> y=y. +intros * H; +(* This worked as expected *) +subst. +Fail clear H. +Abort. + +Goal forall y, let x:=0 in x=y -> y=y. +intros * H; +(* Before the fix, this unfolded x instead of + substituting y and erasing H *) +subst. +Fail clear H. +Abort. |