diff options
| author | Gaëtan Gilbert | 2019-10-13 15:49:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-14 10:24:26 +0200 |
| commit | 26e8b5a545bcf2209d56494ccf4afe143f761fd7 (patch) | |
| tree | 92cd82dc41339a12b960661ef2d36a4fcb8274a4 /library | |
| parent | 81216e8947fb4906f5a2b109cbed3e2584383c57 (diff) | |
Remove [in_section] arguments to Safe_typing functions
The information is already there.
At some point we may want to clean up the Lib API to reduce redundancy
wrt kernel functions like [sections_are_opened], but I'm not doing now
as it would conflict with https://github.com/coq/coq/pull/10670
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 5 | ||||
| -rw-r--r-- | library/global.mli | 6 |
2 files changed, 7 insertions, 4 deletions
diff --git a/library/global.ml b/library/global.ml index c4685370d1..24cfc57f28 100644 --- a/library/global.ml +++ b/library/global.ml @@ -102,8 +102,8 @@ let typing_flags () = Environ.typing_flags (env ()) let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) -let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) -let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d) +let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) +let add_constant ~side_effect id d = globalize (Safe_typing.add_constant ~side_effect (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) @@ -111,6 +111,7 @@ let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) let open_section () = globalize0 Safe_typing.open_section let close_section fs = globalize0_with_summary fs Safe_typing.close_section +let sections_are_opened () = Safe_typing.sections_are_opened (safe_env()) let start_module id = globalize (Safe_typing.start_module (i2l id)) let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) diff --git a/library/global.mli b/library/global.mli index c45bf65d84..d689771f0a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,12 +46,12 @@ val push_named_assum : (Id.t * Constr.types) -> unit val push_named_def : (Id.t * Entries.section_def_entry) -> unit val push_section_context : (Name.t array * Univ.UContext.t) -> unit -val export_private_constants : in_section:bool -> +val export_private_constants : Safe_typing.private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : - side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a + side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -80,6 +80,8 @@ val close_section : Summary.frozen -> unit (** Close the section and reset the global state to the one at the time when the section what opened. *) +val sections_are_opened : unit -> bool + (** Interactive modules and module types *) val start_module : Id.t -> ModPath.t |