diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 0926d35f6..ce05190b6 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -60,6 +60,7 @@ open Util open Names open Declarations +open Context.Named.Declaration (** {6 Safe environments } @@ -222,13 +223,6 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) -let constant_entry_of_private_constant = function - | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> - [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ] - | { Entries.eff = Entries.SEscheme (l,_) } -> - List.map (fun (_,kn,cb,eff_env) -> - kn, Term_typing.constant_entry_of_side_effect cb eff_env) l - let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in { Entries.from_env = CEphemeron.create env.revstruct; @@ -369,7 +363,8 @@ let check_required current_libs needed = hypothesis many many times, and the check performed here would cost too much. *) -let safe_push_named (id,_,_ as d) env = +let safe_push_named d env = + let id = get_id d in let _ = try let _ = Environ.lookup_named id env in @@ -390,13 +385,13 @@ let push_named_def (id,de) senv = (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o) | _ -> assert false in let senv' = push_context_set poly univs senv in - let env'' = safe_push_named (id,Some c,typ) senv'.env in + let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in univs, {senv' with env=env''} let push_named_assum ((id,t,poly),ctx) senv = let senv' = push_context_set poly ctx senv in let t = Term_typing.translate_local_assum senv'.env t in - let env'' = safe_push_named (id,None,t) senv'.env in + let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in {senv' with env=env''} @@ -561,6 +556,7 @@ let add_mind dir l mie senv = let add_modtype l params_mte inl senv = let mp = MPdot(senv.modpath, l) in let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte in + let mtb = Declareops.hcons_module_body mtb in let senv' = add_field (l,SFBmodtype mtb) MT senv in mp, senv' @@ -581,6 +577,7 @@ let full_add_module_type mp mt senv = let add_module l me inl senv = let mp = MPdot(senv.modpath, l) in let mb = Mod_typing.translate_module senv.env mp inl me in + let mb = Declareops.hcons_module_body mb in let senv' = add_field (l,SFBmodule mb) M senv in let senv'' = if Modops.is_functor mb.mod_type then senv' |