diff options
| author | Pierre-Marie Pédrot | 2019-07-29 10:48:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 22:14:34 +0200 |
| commit | 58a9de2acacb05291d87fe2b656728ae05d59df4 (patch) | |
| tree | 6472556f7796bf6b8364b61ddcadd942ae6f2763 /kernel/safe_typing.mli | |
| parent | 6176c2879dd989029a83642caec7cd66a2a4f527 (diff) | |
Move the Lib section data into the kernel.
Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 4eef43b193..10fedc2faf 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -33,6 +33,8 @@ val is_initial : safe_environment -> bool val env_of_safe_env : safe_environment -> Environ.env +val sections_of_safe_env : safe_environment -> Section.t + (** The safe_environment state monad *) type safe_transformer0 = safe_environment -> safe_environment @@ -67,15 +69,6 @@ val join_safe_environment : val is_joined_environment : safe_environment -> bool (** {6 Enriching a safe environment } *) -(** Insertion of local declarations (Local or Variables) *) - -val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 - -(** Returns the full universe context necessary to typecheck the definition - (futures are forced) *) -val push_named_def : - Id.t * Entries.section_def_entry -> safe_transformer0 - (** Insertion of global axioms or definitions *) type 'a effect_entry = @@ -146,6 +139,16 @@ val open_section : poly:bool -> safe_transformer0 val close_section : safe_transformer0 +(** Insertion of local declarations (Local or Variables) *) + +val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 + +val push_named_def : + Id.t * Entries.section_def_entry -> safe_transformer0 + +(** Add local universes to a polymorphic section *) +val push_section_context : (Name.t array * Univ.UContext.t) -> safe_transformer0 + (** {6 Interactive module functions } *) val start_module : Label.t -> ModPath.t safe_transformer |