diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/ltac.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 9eb5dda721..3f25f70354 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -168,3 +168,10 @@ Goal forall a b c, a=0 -> b=c+a. intros. revert a b c H. Abort. + +(* Used to fail until revision 9280 because of a parasitic App node with + empty args *) + +Goal True. +match None with @None => exact I end. +Abort. |