diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_4502.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_4502.v b/test-suite/bugs/closed/bug_4502.v new file mode 100644 index 0000000000..f1dcae9773 --- /dev/null +++ b/test-suite/bugs/closed/bug_4502.v @@ -0,0 +1,17 @@ +Require Import FunInd. + +Set Universe Polymorphism. +Set Primitive Projections. +Set Implicit Arguments. +Set Strongly Strict Implicit. + +Function first_false (n : nat) (f : nat -> bool) : option nat := + match n with + | O => None + | S m => + match first_false m f with + | (Some _) as s => s + | None => if f m then None else Some m + end + end. +(* undefined universe *) |