From 66973ce17e32a3c692a5b0032f38300ec8cc36d3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Mar 2018 15:10:39 +0100 Subject: Rename some universe minimizing "normalize" functions to "minimize" UState normalize -> minimize, Evd nf_constraints -> minimize_universes --- vernac/vernacentries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/vernacentries.ml') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0ff6d9c17..26c6a8cbe 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -72,7 +72,7 @@ let show_top_evars () = let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in + let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx -- cgit v1.2.3