diff options
| author | Matthieu Sozeau | 2015-09-24 15:19:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:11 +0200 |
| commit | e86b5cf5beab9a67c65afa7456feb417df9d465c (patch) | |
| tree | 91bf036f852fd16d6b4f7c8f26bdb9620291e914 | |
| parent | 11cdf7c2ca0017f6bae906f9c9d9eef41972affe (diff) | |
Univs: fix Show Universes.
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e51dfbaaec..c07c756c01 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -76,9 +76,8 @@ let show_universes () = let gls = Proof.V82.subgoals pfts in 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 (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma)); - msg_notice (str"Normalized constraints: " ++ Univ.pr_universes (Evd.pr_evd_level sigma) cstrs) + msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx) let show_prooftree () = (* Spiwack: proof tree is currently not working *) |