diff options
Diffstat (limited to 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 03acb87a9..d6280e119 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,9 +21,13 @@ type recipe = { d_abstract : Sign.named_context; d_modlist : work_list } -val cook_constant : - env -> recipe -> - constant_def * constant_type * constraints * bool * Sign.section_context +type inline = bool + +type result = + constant_def * constant_type * constraints * inline + * Sign.section_context option + +val cook_constant : env -> recipe -> result (** {6 Utility functions used in module [Discharge]. } *) |