diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1b55293f1c..6e5c9c55ae 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -78,7 +78,8 @@ type 'a effect_entry = | PureEntry : unit effect_entry type global_declaration = - | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration +| ConstantEntry : Entries.constant_entry -> global_declaration +| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration type exported_private_constant = Constant.t |