diff options
| author | Gaëtan Gilbert | 2018-03-02 14:58:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-06 13:41:24 +0100 |
| commit | 5d926b0279f70250db1ee54edcdb4e855ac96f0f (patch) | |
| tree | 06dc436ba2d41764b5bbe48c311bdaeaf5c1514c /engine/termops.ml | |
| parent | 67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff) | |
Deprecate UState aliases in Evd.
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index c615155d1f..35258762a7 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -294,12 +294,11 @@ let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_cont let pr_evar_universe_context ctx = let open UState in - let open Evd in let prl = pr_uctx_level ctx in if UState.is_empty ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++ + h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ |