From 25460d19599fd64aaeccbf4667737feb786ae7f6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 21 Nov 2013 13:06:39 +0100
Subject: - Fix Check to use the constraints inferred during type inference. -
 Fix declaration of projections to work again with Primitive Projections on.

Conflicts:
	kernel/term_typing.ml
---
 toplevel/vernacentries.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 67ca1b666f..450b6ee51f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1387,6 +1387,8 @@ let vernac_check_may_eval redexp glopt rc =
   let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
+  let uctx = Evd.universe_context sigma' in
+  let env = Environ.push_context uctx env in
   let c = nf c in
   let j =
     try
@@ -1396,7 +1398,7 @@ let vernac_check_may_eval redexp glopt rc =
       Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in
   match redexp with
     | None ->
-	msg_notice (print_judgment env j)
+	msg_notice (print_judgment env j ++ Printer.pr_universe_ctx uctx)
     | Some r ->
         Tacintern.dump_glob_red_expr r;
         let (sigma',r_interp) = interp_redexp env sigma' r in
@@ -1415,7 +1417,8 @@ let vernac_global_check c =
   let senv = Global.safe_env() in
   let senv = Safe_typing.add_constraints (snd ctx) senv in
   let j = Safe_typing.typing senv c in
-  msg_notice (print_safe_judgment env j)
+  let env = Safe_typing.env_of_safe_env senv in
+    msg_notice (print_safe_judgment env j)
 
 let vernac_print = function
   | PrintTables -> msg_notice (print_tables ())
-- 
cgit v1.2.3