diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_13278.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_13278.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v index 44a14174cd..9831a4d205 100644 --- a/test-suite/bugs/closed/bug_13278.v +++ b/test-suite/bugs/closed/bug_13278.v @@ -6,3 +6,10 @@ Goal even 1 -> False. Proof. refine (fun a => match a with end). Qed. + +Goal even 1 -> False. +Proof. + refine (fun a => match a in even n + return match n with 1 => False | _ => True end : Prop + with evenB => I | evenS _ _ => I end). +Qed. |