diff options
| author | Pierre-Marie Pédrot | 2019-05-22 17:46:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-26 01:14:38 +0200 |
| commit | 1e83ae578feea41d34c3ba26a1f74c3c715620a2 (patch) | |
| tree | c67f5fd826c315191bfa666cd5e025ff396534cc /kernel/safe_typing.mli | |
| parent | 51dc650f8b47a7381c19376793871817f2ef9578 (diff) | |
More precise type for Safe_typing export and inlining of private constants.
We get rid of the future wrappers, as all callers are immediately forcing
the result.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 36ca3d8c47..770caf5406 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -49,10 +49,8 @@ val concat_private : private_constants -> private_constants -> private_constants [e1] must be more recent than those of [e2]. *) val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output -val inline_private_constants_in_constr : - Environ.env -> Constr.constr -> private_constants -> Constr.constr -val inline_private_constants_in_definition_entry : - Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry +val inline_private_constants : + Environ.env -> private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set val push_private_constants : Environ.env -> private_constants -> Environ.env (** Push the constants in the environment if not already there. *) @@ -93,8 +91,8 @@ type exported_private_constant = Constant.t * Entries.side_effect_role val export_private_constants : in_section:bool -> - private_constants Entries.definition_entry -> - (unit Entries.definition_entry * exported_private_constant list) safe_transformer + private_constants Entries.proof_output -> + (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer (** returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported) *) |