diff options
| author | Gaëtan Gilbert | 2019-10-01 10:12:33 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-01 10:12:33 +0200 |
| commit | 77fd11a9f012a2878e13451e9d8a9f500c6392eb (patch) | |
| tree | b8440203d6eb46a6af050e493661a0a29bf19233 /kernel/safe_typing.mli | |
| parent | 41f3d8f0b0b6efbb7133cd4e44c70a1d9105c3e9 (diff) | |
| parent | 7e70815c2f326518c71f25fd9b222281a757572b (diff) | |
Merge PR #10797: Implement discharging in kernel
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
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 : |