diff options
| author | Pierre-Marie Pédrot | 2019-09-26 11:14:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-26 15:29:41 +0200 |
| commit | 92006b6cc6b49ed6f892a7e5475f32ca852a9769 (patch) | |
| tree | 7884eb1bbb64981b7545fffcb8cb3f604f8a8561 /kernel/safe_typing.mli | |
| parent | 884b413e91d293a6b2009da11f2996db0654e40f (diff) | |
Implement section discharging inside kernel.
This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 10fedc2faf..d3ca642a89 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -27,13 +27,15 @@ val digest_match : actual:vodigest -> required:vodigest -> bool type safe_environment +type section_data + val empty_environment : safe_environment val is_initial : safe_environment -> bool val env_of_safe_env : safe_environment -> Environ.env -val sections_of_safe_env : safe_environment -> Section.t +val sections_of_safe_env : safe_environment -> section_data Section.t (** The safe_environment state monad *) @@ -89,9 +91,6 @@ val add_constant : side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> (Constant.t * 'a) safe_transformer -val add_recipe : - in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer - (** Adding an inductive type *) val add_mind : |