diff options
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 : |