diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Inversion.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 5091b44c1c..043d949c91 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -129,3 +129,10 @@ Proof. an inconsistent state that disturbed "inversion" *) intros. inversion H. Abort. + +(* Bug #2314 (simplified): check that errors do not show as anomalies *) + +Goal True -> True. +intro. +Fail inversion H using False. +Fail inversion foo using True_ind. |