From a48cefa07907120c2270bf7a7689fa00a5adc167 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Dec 2017 15:54:53 +0100
Subject: Fix anomaly in [Type foo] command, + print uctx like Check.

---
 test-suite/success/Check.v | 2 ++
 vernac/vernacentries.ml    | 9 +++++----
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 0f677a8495..82b51b1ffb 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -12,3 +12,5 @@
 Check 0.
 Check S.
 Check nat.
+
+Type Type : Type.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 63768d9b88..62b6396b4f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1591,13 +1591,14 @@ let vernac_declare_reduction ~atts s r =
 let vernac_global_check c =
   let env = Global.env() in
   let sigma = Evd.from_env env in
-  let c,ctx = interp_constr env sigma c in
+  let c,uctx = interp_constr env sigma c in
   let senv = Global.safe_env() in
-  let cstrs = snd (UState.context_set ctx) in
-  let senv = Safe_typing.add_constraints cstrs senv in
+  let uctx = UState.context_set uctx in
+  let senv = Safe_typing.push_context_set false uctx senv in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in
-    Feedback.msg_notice (print_safe_judgment env sigma j)
+  Feedback.msg_notice (print_safe_judgment env sigma j ++
+                       pr_universe_ctx_set sigma uctx)
 
 
 let get_nth_goal n =
-- 
cgit v1.2.3