From 925794c34d08752cee85362d1c2772559e89d2c9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 11 Jan 2021 12:12:45 +0100
Subject: 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.
---
 test-suite/bugs/closed/bug_13732.v | 16 ++++++++++++++++
 vernac/vernacentries.ml            |  5 ++++-
 2 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_13732.v

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.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4f3fc46c12..5f2b352a9c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1458,7 +1458,10 @@ let vernac_reserve bl =
     let env = Global.env() in
     let sigma = Evd.from_env env in
     let t,ctx = Constrintern.interp_type env sigma c in
-    let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t in
+    let t = Flags.without_option Detyping.print_universes (fun () ->
+        Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t)
+        ()
+    in
     let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl
-- 
cgit v1.2.3