diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 715226107..148fdca67 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -103,7 +103,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * unit Entries.constant_entry * private_constant_role + constant * private_constant_role val export_private_constants : in_section:bool -> private_constants Entries.constant_entry -> |