aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
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 () =