diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_13278.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v new file mode 100644 index 0000000000..44a14174cd --- /dev/null +++ b/test-suite/bugs/closed/bug_13278.v @@ -0,0 +1,8 @@ +Inductive even: nat -> Prop := +| evenB: even 0 +| evenS: forall n, even n -> even (S (S n)). + +Goal even 1 -> False. +Proof. + refine (fun a => match a with end). +Qed. |