diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-15 17:46:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:52 +0200 |
| commit | 3fcf0930874d7200f2503ac7084b1d6669d59540 (patch) | |
| tree | f4801ab2074dbcf21f691230ae1ea83dff2fc71a /kernel/safe_typing.mli | |
| parent | 3c6679676c3963b7c3ec7c1eadbf24ae70311408 (diff) | |
Remove a horrendous hack in Declare to retrieve exported side-effects.
Instead of relying on a mutable state in the object pushed on the libstack,
we export an API in the kernel that exports the side-effects of a given
entry in the global environment.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 2a454400f..715226107 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -95,7 +95,7 @@ val push_named_def : (** Insertion of global axioms or definitions *) type 'a effect_entry = -| EffectEntry : bool -> private_constants effect_entry (* bool: export private constants *) +| EffectEntry : private_constants effect_entry | PureEntry : unit effect_entry type global_declaration = @@ -105,11 +105,15 @@ type global_declaration = type exported_private_constant = constant * unit Entries.constant_entry * private_constant_role +val export_private_constants : in_section:bool -> + private_constants Entries.constant_entry -> + (unit Entries.constant_entry * exported_private_constant list) safe_transformer + (** returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported) *) val add_constant : DirPath.t -> Label.t -> global_declaration -> - (constant * exported_private_constant list) safe_transformer + constant safe_transformer (** Adding an inductive type *) |