diff options
| author | Pierre-Marie Pédrot | 2019-05-16 00:02:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-20 14:10:58 +0200 |
| commit | 27468ae02bbbf018743d53a9db49efa34b6d6a3e (patch) | |
| tree | e8fa5ad95ba323d76af06d24e9d804a0dae94844 /kernel/safe_typing.mli | |
| parent | 801aed67a90ec49c15a4469e1905aa2835fabe19 (diff) | |
Ensure statically that declarations built by Term_typing are direct.
This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b9a68663d3..36ca3d8c47 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -88,7 +88,6 @@ type 'a effect_entry = type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration - | GlobalRecipe of Cooking.recipe type exported_private_constant = Constant.t * Entries.side_effect_role @@ -103,6 +102,9 @@ val add_constant : ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration -> (Constant.t * private_constants) safe_transformer +val add_recipe : + in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer + (** Adding an inductive type *) val add_mind : |