Fix #13732: Implicit Type vs universes

This returns to the previous behaviour of Implicit Type forgetting
universes.

`Implicit Type T : Type@{u}.` may be confusing as it is equivalent to
`: Type`, but until we have a better idea of what to do with anonymous
types I see no other solution, especially in the short term to fix the
bug.

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.