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 0faaa275f..8e9be2e40 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -369,3 +369,10 @@ intros. destruct (H _). change (0=0) in H0. (* Check generalization on H0 was made *) Abort. + +(* Check absence of anomaly (failed at some time) *) + +Goal forall A (a:A) (P Q:A->Prop), (forall a, P a -> Q a) -> True. +intros. +Fail destruct H. +Abort. |