From ba2ad4fdcfb7e56a71c5797b82644cc9a49dd18f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 19 Dec 2014 14:42:09 +0100
Subject: In Show Universes, print universes before normalization.

---
 toplevel/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3d2052c3bc..3b7a8ae479 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -77,7 +77,7 @@ let show_universes () =
   let sigma = gls.Evd.sigma in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
   let cstrs = Univ.merge_constraints (Univ.ContextSet.constraints ctx) Univ.empty_universes in
-    msg_notice (Univ.pr_universe_context_set ctx);
+    msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
     msg_notice (str"Normalized constraints: " ++ Univ.pr_universes cstrs)
 
 let show_prooftree () =
-- 
cgit v1.2.3