1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3354.v b/test-suite/bugs/closed/3354.v
new file mode 100644
index 00000000..14b66db3
--- /dev/null
+++ b/test-suite/bugs/closed/3354.v
@@ -0,0 +1,12 @@
+Set Universe Polymorphism.
+Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
+Inductive Empty : Type1 := .
+Fail Check Empty : Set.
+(* Toplevel input, characters 15-116:
+Error: Conversion test raised an anomaly *)
+(* Now we make sure it's not an anomaly *)
+Goal True.
+Proof.
+  try exact (let x := Empty : Set in I).
+  exact I.
+Defined.