From 11231a495cc3dc2b8a754dac77d7739c5b54ac30 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Oct 2019 13:09:29 +0100
Subject: add test for #4502 (fixed by unknown commit)

Close #4502
---
 test-suite/bugs/closed/bug_4502.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_4502.v

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 *)
-- 
cgit v1.2.3