diff options
| author | Maxime Dénès | 2018-03-08 21:22:59 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-08 21:22:59 +0100 |
| commit | a40fb961c8ffeeb03769404cacda8bd6cff17417 (patch) | |
| tree | 7105d621bc16f825c1f309e3d5b7720b1b1513ec /engine/termops.ml | |
| parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
| parent | 66973ce17e32a3c692a5b0032f38300ec8cc36d3 (diff) | |
Merge PR #6893: Cleanup UState API usage
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)++ |