diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-15 18:34:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-16 14:31:01 +0100 |
| commit | 25f09e86ba1a3ab3c24d5e17336b01315a205e00 (patch) | |
| tree | b3cdbae6081b4f414bf131e61f9da5891941ea39 /library/global.mli | |
| parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) | |
Let definitions must not contain side-effects when reaching the kernel.
Let definitions have the same behaviour if they are ended with a Qed or a
Defined command, i.e. they are treated as if they were transparent. Indeed,
it doesn't make sense for them to be opaque as they are going to be expanded
away at the end of the section.
For an unknown reason, handling of side-effects in Let definitions considers
them as if they were opaque, i.e. the effects are inlined in the definition.
This discrepancy has bad consequences in the kernel, where one is forced to
juggle with universe constraints generated by polymorphic Let definitions.
As a first phase of cleaning, we simply enforce by typing that Let definitions
should be purified before reaching the kernel.
This has the intended side-effect to make side-effects persistent in Let
definitions, as if they were indeed truly transparent.
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/global.mli b/library/global.mli index 324181e79..2a646386e 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,11 +32,11 @@ val set_typing_flags : Declarations.typing_flags -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.ContextSet.t +val push_named_def : (Id.t * unit Entries.definition_entry) -> Univ.ContextSet.t val export_private_constants : in_section:bool -> - Safe_typing.private_constants Entries.constant_entry -> - unit Entries.constant_entry * Safe_typing.exported_private_constant list + Safe_typing.private_constants Entries.definition_entry -> + unit Entries.definition_entry * Safe_typing.exported_private_constant list val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t |