diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-11-21 13:06:39 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:56 +0200 |
| commit | 25460d19599fd64aaeccbf4667737feb786ae7f6 (patch) | |
| tree | c297a08dbe18e06f0bf11015380b156a3ce2a162 /toplevel | |
| parent | ea47d7fb0b8ed663ecda142fe74bcbcfec3bb554 (diff) | |
- Fix Check to use the constraints inferred during type inference.
- Fix declaration of projections to work again with Primitive Projections on.
Conflicts:
kernel/term_typing.ml
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 ()) |