Merge PR #6449: Let definitions must not contain side-effects when reaching the kernel.

4 files changed, 11 insertions, 16 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5150ad411..fa984515a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -383,8 +383,7 @@ let safe_push_named d env =
 
 let push_named_def (id,de) senv =
   let open Entries in
-  let trust = Term_typing.SideEffects senv.revstruct in
-  let c,typ,univs = Term_typing.translate_local_def trust senv.env id de in
+  let c,typ,univs = Term_typing.translate_local_def senv.env id de in
   let poly = match de.Entries.const_entry_universes with
   | Monomorphic_const_entry _ -> false
   | Polymorphic_const_entry _ -> true
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a30bb37e6..fbc398a2a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -90,7 +90,7 @@ val push_named_assum :
 (** Returns the full universe context necessary to typecheck the definition
   (futures are forced) *)
 val push_named_def :
-  Id.t * private_constants Entries.definition_entry -> Univ.ContextSet.t safe_transformer
+  Id.t * unit Entries.definition_entry -> Univ.ContextSet.t safe_transformer
 
 (** Insertion of global axioms or definitions *)
 
@@ -106,8 +106,8 @@ type exported_private_constant =
   Constant.t * 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
+  private_constants Entries.definition_entry ->
+  (unit Entries.definition_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) *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 70dd6438d..761eab511 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -533,14 +533,10 @@ type side_effect_role =
 type exported_side_effect = 
   Constant.t * constant_body * side_effect_role
 
-let export_side_effects mb env ce =
-  match ce with
-  | ParameterEntry e -> [], ParameterEntry e
-  | ProjectionEntry e -> [], ProjectionEntry e
-  | DefinitionEntry c ->
+let export_side_effects mb env c =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
-      let ce = DefinitionEntry { c with
+      let ce = { c with
         const_entry_body = Future.chain body
           (fun (b_ctx, _) -> b_ctx, ()) } in
       let not_exists (c,_,_,_) =
@@ -609,9 +605,9 @@ let translate_recipe env kn r =
   let hcons = DirPath.is_empty dir in
   build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
 
-let translate_local_def mb env id centry =
+let translate_local_def env id centry =
   let open Cooking in
-  let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
+  let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in
   let typ = decl.cook_type in
   if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
     match decl.cook_body with
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