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 /library | |
| 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 'library')
| -rw-r--r-- | library/global.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/global.mli b/library/global.mli index aa9fc18477..eaa76c3117 100644 --- a/library/global.mli +++ b/library/global.mli @@ -42,8 +42,8 @@ val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set val push_named_def : (Id.t * Entries.section_def_entry) -> unit val export_private_constants : in_section:bool -> - Safe_typing.private_constants Entries.definition_entry -> - unit Entries.definition_entry * Safe_typing.exported_private_constant list + Safe_typing.private_constants Entries.proof_output -> + Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants |