Merge PR #10995: add test for #4502 (fixed by unknown commit)

Reviewed-by: ppedrot

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 *)