diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 67ca1b666..450b6ee51 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1387,6 +1387,8 @@ let vernac_check_may_eval redexp glopt rc = let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in + let uctx = Evd.universe_context sigma' in + let env = Environ.push_context uctx env in let c = nf c in let j = try @@ -1396,7 +1398,7 @@ let vernac_check_may_eval redexp glopt rc = Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in match redexp with | None -> - msg_notice (print_judgment env j) + msg_notice (print_judgment env j ++ Printer.pr_universe_ctx uctx) | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in @@ -1415,7 +1417,8 @@ let vernac_global_check c = let senv = Global.safe_env() in let senv = Safe_typing.add_constraints (snd ctx) senv in let j = Safe_typing.typing senv c in - msg_notice (print_safe_judgment env j) + let env = Safe_typing.env_of_safe_env senv in + msg_notice (print_safe_judgment env j) let vernac_print = function | PrintTables -> msg_notice (print_tables ()) |