diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/destruct.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 90a60daa66..ea939f0855 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -430,3 +430,9 @@ eexists ?[x]. destruct (S _). change (0 = ?x). Abort. + +Goal (forall P, P 0 -> True/\True) -> True. +intro H. +destruct (H (fun x => True)). +match goal with |- True => idtac end. +Abort. |