1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13732.v b/test-suite/bugs/closed/bug_13732.v
new file mode 100644
index 0000000000..24840abdf6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13732.v
@@ -0,0 +1,16 @@
+Module Sort.
+  Set Printing Universes.
+
+  Implicit Types TT : Type.
+
+  Check fun TT => nat.
+End Sort.
+
+Module Ref.
+  Set Universe Polymorphism.
+
+  Axiom tele : Type.
+
+  Implicit Types TT : tele.
+  Check fun TT => nat.
+End Ref.