diff options
| -rw-r--r-- | kernel/term_typing.ml | 32 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
2 files changed, 31 insertions, 8 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c655e2f33..dc2ddea4a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -124,12 +124,32 @@ let infer_declaration env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let body, side_eff = Future.join body in let body = handle_side_effects env body side_eff in - let j = infer env body in - let j = hcons_j j in - let typ = constrain_type env j c.const_entry_polymorphic (map_option_typ typ) in - feedback_completion_typecheck feedback_id; - let def = Def (Mod_subst.from_val j.uj_val) in - def, typ, None, c.const_entry_polymorphic, + let def, typ, proj = + match c.const_entry_proj with + | Some (ind, n, m, ty) -> + (* FIXME: check projection *) + let pb = { proj_ind = ind; + proj_npars = n; + proj_arg = m; + proj_type = ty; + proj_body = body } + in + let body' = mkProj (Option.get kn, mkRel 1) in + (* TODO: recognize projection *) + let context, m = decompose_lam_n_assum (n + 1) body in + let body = it_mkLambda_or_LetIn body' context in + (* let tj = infer_type env' (Option.get c.const_entry_type) in *) + Def (Mod_subst.from_val (hcons_constr body)), + RegularArity (hcons_constr (Option.get typ)), Some pb + | None -> + let j = infer env body in + let j = hcons_j j in + let typ = constrain_type env j c.const_entry_polymorphic (map_option_typ typ) in + let def = Def (Mod_subst.from_val j.uj_val) in + def, typ, None + in + feedback_completion_typecheck feedback_id; + def, typ, proj, c.const_entry_polymorphic, c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx let global_vars_set_constant_type env = function 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 ()) |