diff options
| author | Maxime Dénès | 2019-05-27 16:10:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-27 16:10:18 +0200 |
| commit | e005f390312b8900df36aa27bc087e18701c8fcd (patch) | |
| tree | 41d0ceab9484a261c686e665967223c66befca78 /library | |
| parent | c371b6f0bc6aa75fb3fe138d2bd52bdd189550b1 (diff) | |
| parent | 1e83ae578feea41d34c3ba26a1f74c3c715620a2 (diff) | |
Merge PR #10249: More precise type for export and inlining of private constants
Reviewed-by: gares
Ack-by: maximedenes
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 |