diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 849b1d47d6..61ebc9bbe6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1563,7 +1563,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 ctx) in + let cstrs = snd (Evd.evar_universe_context_set Univ.UContext.empty 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 @@ -1628,9 +1628,13 @@ let vernac_print = function msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) | PrintUniverses (b, None) -> - let univ = Global.universes () in - let univ = if b then Univ.sort_universes univ else univ in - msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ) + let univ = Global.universes () in + let univ = if b then Univ.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 + msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) | PrintUniverses (b, Some s) -> dump_universes b s | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) |