export_private_constants doesn't use the [constr in_univ_ctx] argument

4 files changed, 12 insertions, 12 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f6f2058c13..2047fd5fc5 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -757,7 +757,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
@@ -774,7 +774,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 =
@@ -803,8 +803,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
@@ -817,7 +817,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 92bbd264fa..c879481c66 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -84,8 +84,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..e1d2ccc3eb 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -299,7 +299,7 @@ let define_constant ~name cd =
     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 = Global.export_private_constants 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
@@ -377,8 +377,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 ((body, uctx), eff) = Future.force de.proof_entry_body in
+      let export = Global.export_private_constants eff.Evd.seff_private in
       let eff = get_roles export eff in
       let () = List.iter register_side_effect eff in
       let poly, univs = match de.proof_entry_universes with