Merge PR #11491: Small side effect cleanup

Reviewed-by: ejgallego
Reviewed-by: ppedrot

4 files changed, 47 insertions, 45 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e8adde2605..8db8a044a8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -759,7 +759,7 @@ let translate_direct_opaque env kn ce =
   let () = assert (is_empty_private u) in
   { cb with const_body = OpaqueDef c }
 
-let export_side_effects mb env (b_ctx, eff) =
+let export_side_effects mb env eff =
       let not_exists e = not (Environ.mem_constant e.seff_constant env) in
       let aux (acc,sl) e =
         if not (not_exists e) then acc, sl
@@ -776,7 +776,7 @@ let export_side_effects mb env (b_ctx, eff) =
       in
       let rec translate_seff sl seff acc env =
         match seff with
-        | [] -> List.rev acc, b_ctx
+        | [] -> List.rev acc
         | eff :: rest ->
           if Int.equal sl 0 then
             let env, cb =
@@ -805,8 +805,8 @@ let push_opaque_proof pf senv =
   let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
   senv, o
 
-let export_private_constants ce senv =
-  let exported, ce = export_side_effects senv.revstruct senv.env ce in
+let export_private_constants eff senv =
+  let exported = export_side_effects senv.revstruct senv.env eff in
   let map senv (kn, c) = match c.const_body with
   | OpaqueDef p ->
     let local = empty_private c.const_universes in
@@ -819,7 +819,7 @@ let export_private_constants ce senv =
   let exported = List.map (fun (kn, _) -> kn) exported in
   (* No delayed constants to declare *)
   let senv = List.fold_left add_constant_aux senv bodies in
-  (ce, exported), senv
+  exported, senv
 
 let add_constant l decl senv =
   let kn = Constant.make2 senv.modpath l in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index e6f2fc4a5d..e472dfd5e5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -86,8 +86,8 @@ type side_effect_declaration =
 type exported_private_constant = Constant.t
 
 val export_private_constants :
-  private_constants Entries.proof_output ->
-  (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
+  private_constants ->
+  exported_private_constant list safe_transformer
 
 (** returns the main constant *)
 val add_constant :
diff --git a/library/global.mli b/library/global.mli
index a38fde41a5..b6bd69c17c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -47,8 +47,8 @@ val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
 val push_section_context : (Name.t array * Univ.UContext.t) -> unit
 
 val export_private_constants :
-  Safe_typing.private_constants Entries.proof_output ->
-  Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
+  Safe_typing.private_constants ->
+  Safe_typing.exported_private_constant list
 
 val add_constant :
   Id.t -> Safe_typing.global_declaration -> Constant.t
diff --git a/tactics/declare.ml b/tactics/declare.ml
index c7581fb0e0..ce2f3ec2c5 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -160,6 +160,18 @@ let register_side_effect (c, role) =
   | None -> ()
   | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|]
 
+let get_roles export eff =
+  let map c =
+    let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
+    (c, role)
+  in
+  List.map map export
+
+let export_side_effects eff =
+  let export = Global.export_private_constants eff.Evd.seff_private in
+  let export = get_roles export eff in
+  List.iter register_side_effect export
+
 let record_aux env s_ty s_bo =
   let open Environ in
   let in_ty = keep_hyps env s_ty in
@@ -278,13 +290,6 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
     opaque_entry_universes = univs;
   }
 
-let get_roles export eff =
-  let map c =
-    let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
-    (c, role)
-  in
-  List.map map export
-
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 
 let is_unsafe_typing_flags () =
@@ -293,37 +298,36 @@ let is_unsafe_typing_flags () =
 
 let define_constant ~name cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
-  let export, decl, unsafe = match cd with
-  | DefinitionEntry de ->
-    (* We deal with side effects *)
-    if not de.proof_entry_opaque then
-      (* This globally defines the side-effects in the environment. *)
-      let body, eff = Future.force de.proof_entry_body in
-      let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in
-      let export = get_roles export eff in
-      let de = { de with proof_entry_body = Future.from_val (body, ()) } in
-      let cd = Entries.DefinitionEntry (cast_proof_entry de) in
-      export, ConstantEntry cd, false
-    else
-      let map (body, eff) = body, eff.Evd.seff_private in
-      let body = Future.chain de.proof_entry_body map in
-      let de = { de with proof_entry_body = body } in
-      let de = cast_opaque_proof_entry EffectEntry de in
-      [], OpaqueEntry de, false
-  | ParameterEntry e ->
-    [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
-  | PrimitiveEntry e ->
-    [], ConstantEntry (Entries.PrimitiveEntry e), false
+  let decl, unsafe = match cd with
+    | DefinitionEntry de ->
+      (* We deal with side effects *)
+      if not de.proof_entry_opaque then
+        let body, eff = Future.force de.proof_entry_body in
+        (* This globally defines the side-effects in the environment
+           and registers their libobjects. *)
+        let () = export_side_effects eff in
+        let de = { de with proof_entry_body = Future.from_val (body, ()) } in
+        let cd = Entries.DefinitionEntry (cast_proof_entry de) in
+        ConstantEntry cd, false
+      else
+        let map (body, eff) = body, eff.Evd.seff_private in
+        let body = Future.chain de.proof_entry_body map in
+        let de = { de with proof_entry_body = body } in
+        let de = cast_opaque_proof_entry EffectEntry de in
+        OpaqueEntry de, false
+    | ParameterEntry e ->
+      ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
+    | PrimitiveEntry e ->
+      ConstantEntry (Entries.PrimitiveEntry e), false
   in
   let kn = Global.add_constant name decl in
   if unsafe || is_unsafe_typing_flags() then feedback_axiom();
-  kn, export
+  kn
 
 let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
   let () = check_exists name in
-  let kn, export = define_constant ~name cd in
-  (* Register the libobjects attached to the constants and its subproofs *)
-  let () = List.iter register_side_effect export in
+  let kn = define_constant ~name cd in
+  (* Register the libobjects attached to the constants *)
   let () = register_constant kn kind local in
   kn
 
@@ -377,10 +381,8 @@ let declare_variable ~name ~kind d =
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
-      let (body, eff) = Future.force de.proof_entry_body in
-      let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in
-      let eff = get_roles export eff in
-      let () = List.iter register_side_effect eff in
+      let ((body, uctx), eff) = Future.force de.proof_entry_body in
+      let () = export_side_effects eff in
       let poly, univs = match de.proof_entry_universes with
         | Monomorphic_entry uctx -> false, uctx
         | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx