Fix anomaly in [Type foo] command, + print uctx like Check.

2 files changed, 7 insertions, 4 deletions

diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 0f677a849..82b51b1ff 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 63768d9b8..62b6396b4 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 =