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 /kernel/safe_typing.mli | |
| 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 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index d97d61a72f..1b55293f1c 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -82,13 +82,13 @@ type global_declaration = type exported_private_constant = Constant.t -val export_private_constants : in_section:bool -> +val export_private_constants : private_constants Entries.proof_output -> (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer (** returns the main constant plus a certificate of its validity *) val add_constant : - side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> + side_effect:'a effect_entry -> Label.t -> global_declaration -> (Constant.t * 'a) safe_transformer (** Adding an inductive type *) @@ -138,6 +138,8 @@ val open_section : safe_transformer0 val close_section : safe_transformer0 +val sections_are_opened : safe_environment -> bool + (** Insertion of local declarations (Local or Variables) *) val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 |