diff options
| author | Pierre-Marie Pédrot | 2019-06-25 20:57:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-08 20:47:26 +0200 |
| commit | d929838be77e30db04cd91201542bb52ed3ff7fd (patch) | |
| tree | 81a49bd4863424b841963f46025409396756d0bf /kernel/safe_typing.mli | |
| parent | 75de485c233dd7bbb6301b49e6702eee205977fb (diff) | |
Similar purity invariants in the kernel.
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 = |