From 25f09e86ba1a3ab3c24d5e17336b01315a205e00 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 15 Dec 2017 18:34:43 +0100 Subject: 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. --- kernel/term_typing.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/term_typing.mli') diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 55da4197e..c771452a1 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -18,7 +18,7 @@ type _ trust = | Pure : unit trust | SideEffects : structure_body -> side_effects trust -val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry -> +val translate_local_def : env -> Id.t -> unit definition_entry -> constant_def * types * Univ.ContextSet.t val translate_local_assum : env -> types -> types @@ -62,8 +62,8 @@ type exported_side_effect = * be pushed in the safe_env by safe typing. The main constant entry * needs to be translated as usual after this step. *) val export_side_effects : - structure_body -> env -> side_effects constant_entry -> - exported_side_effect list * unit constant_entry + structure_body -> env -> side_effects definition_entry -> + exported_side_effect list * unit definition_entry val translate_mind : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body -- cgit v1.2.3