diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2817.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/shouldsucceed/2817.v index 25ac15574c..08dff99287 100644 --- a/test-suite/bugs/closed/shouldsucceed/2817.v +++ b/test-suite/bugs/closed/shouldsucceed/2817.v @@ -5,4 +5,5 @@ Goal forall (f: nat -> nat -> Prop) (x:bool) (H0: forall x0, f (if x then x0 else x0) x0), False. -intros; apply H in H0. (* crashes *) +intros. +Fail apply H in H0. (* should fail without exhausting the stack *) |