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 c3d0965857..2406b6add1 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -79,7 +79,7 @@ val push_named_def : (** Insertion of global axioms or definitions *) type 'a effect_entry = -| EffectEntry : private_constants effect_entry +| EffectEntry : private_constants Entries.seff_wrap effect_entry | PureEntry : unit effect_entry type global_declaration = |