diff options
| author | Hugo Herbelin | 2014-10-27 08:03:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-27 09:57:11 +0100 |
| commit | 47828f078ac7359e8e2e1891bc6ef48812bb73a5 (patch) | |
| tree | a64c89566525ff42618ff32736c5a3b6e8979705 /test-suite | |
| parent | be5db64b2478a45f0d6bf183b502bc44de709465 (diff) | |
Ensuring compatibility when an hypothesis used for destruct is
dependent in the goal without being fully applied: it cannot be
erased. This used to work in 8.4 when the hypothesis was in an empty
type. I fixed this and (somehow arbitrarily) generalized the
non-erasing to other inductive types instead of failing.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/destruct.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 26dab73ef6..4704a08e59 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -235,3 +235,20 @@ intro a. destruct a. change (0 = a 1). Abort. + +(* This example of a variable not fully applied in the goal was working in 8.4*) + +Goal forall H : 0<>0, H = H. +destruct H. +reflexivity. +Qed. + +(* Check that variables not fully applied in the goal are not erased + (this example was failing in 8.4 because of a forbidden "clear H" in + the code of "destruct H" *) + +Goal forall H : True -> True, H = H. +destruct H. +- exact I. +- reflexivity. +Qed. |