diff options
| author | Pierre-Marie Pédrot | 2019-10-16 16:27:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-16 16:27:53 +0200 |
| commit | cc9856e33fa1a15fe699e8d9cd7b76086563683d (patch) | |
| tree | 3a51c6466ff40685d2c126a3997390c227b2ce8b /kernel/safe_typing.mli | |
| parent | 5d82451d6d6f591ad81919d8e6529cee48474b9e (diff) | |
| parent | afd214869f050d07f9774d770c289bdc6e602dfd (diff) | |
Merge PR #10885: Remove [in_section] arguments to Safe_typing functions
Reviewed-by: ejgallego
Reviewed-by: ppedrot
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 |