diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/destruct.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index c6eff3eebe..66629f7fd3 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -277,3 +277,15 @@ Abort. Goal forall f : A -> nat -> nat, f a 0 = f a 1. intros. destruct f. + +(* This one was not working in 8.4 *) + +Section S1. +Variables x y : Type. +Variable H : x = y. +Goal True. +destruct H. (* Was not working in 8.4 *) +(* Now check that H statement has not be itself subject of the rewriting *) +change (x=y) in H. +Abort. +End S1. |