diff options
| author | Matthieu Sozeau | 2014-12-19 14:42:09 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-05 16:39:47 +0100 |
| commit | ba2ad4fdcfb7e56a71c5797b82644cc9a49dd18f (patch) | |
| tree | 652977782be0e9049095b002f70baeb7ce6a4b45 | |
| parent | ce2efc0e02c4d164d9206361c0a2de6123816d00 (diff) | |
In Show Universes, print universes before normalization.
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
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 () = |