diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/destruct.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index ada292f186..02f88b7270 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -29,3 +29,10 @@ Goal forall n, n = S n. induction S. Abort. +(* Check that elimination with remaining evars do not raise an bad + error message *) + +Theorem Refl : forall P, P <-> P. tauto. Qed. +Goal True. +case Refl || ecase Refl. +Abort. |