diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.mli | 7 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 7 |
2 files changed, 6 insertions, 8 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli index f94068f31e..8e8e97d615 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -97,7 +97,12 @@ type module_entry = | MExpr of module_params_entry * module_struct_entry * module_struct_entry option -type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + +type seff_env = + [ `Nothing + (* The proof term and its universes. + Same as the constant_body's but not in an ephemeron *) + | `Opaque of Constr.t * Univ.universe_context_set ] type side_eff = | SEsubproof of constant * Declarations.constant_body * seff_env diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 927278965f..8b28cd87bd 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -222,13 +222,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; |