diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2b2332324..b3512ffde 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -347,7 +347,7 @@ let dump_universes_gen g s = end in try - Univ.dump_universes output_constraint g; + UGraph.dump_universes output_constraint g; close (); msg_info (str "Universes written to file \"" ++ str s ++ str "\".") with reraise -> @@ -1554,7 +1554,7 @@ let vernac_global_check c = let sigma = Evd.from_env env in let c,ctx = interp_constr env sigma c in let senv = Global.safe_env() in - let cstrs = snd (Evd.evar_universe_context_set Univ.UContext.empty ctx) in + let cstrs = snd (UState.context_set ctx) in let senv = Safe_typing.add_constraints cstrs senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in @@ -1620,13 +1620,13 @@ let vernac_print = function | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) | PrintUniverses (b, dst) -> let univ = Global.universes () in - let univ = if b then Univ.sort_universes univ else univ in + let univ = if b then UGraph.sort_universes univ else univ in let pr_remaining = if Global.is_joined_environment () then mt () else str"There may remain asynchronous universe constraints" in begin match dst with - | None -> msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) + | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) | Some s -> dump_universes_gen univ s end | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) |