Merge PR #10299: Lazy substitution of section contexts in opaque proofs

Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

15 files changed, 145 insertions, 108 deletions

diff --git a/checker/check.ml b/checker/check.ml
index c5bc59e72a..903258daef 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -51,7 +51,7 @@ let pr_path sp =
 type compilation_unit_name = DirPath.t
 
 type seg_univ = Univ.ContextSet.t * bool
-type seg_proofs = Constr.constr option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr option) array
 
 type library_t = {
   library_name : compilation_unit_name;
@@ -98,9 +98,19 @@ let access_opaque_table dp i =
     with Not_found -> assert false
   in
   assert (i < Array.length t);
-  t.(i)
+  let (info, n, c) = t.(i) in
+  match c with
+  | None -> None
+  | Some c -> Some (Cooking.cook_constr info n c)
 
-let () = Mod_checking.set_indirect_accessor access_opaque_table
+let access_discharge = Cooking.cook_constr
+
+let indirect_accessor = {
+  Opaqueproof.access_proof = access_opaque_table;
+  Opaqueproof.access_discharge = access_discharge;
+}
+
+let () = Mod_checking.set_indirect_accessor indirect_accessor
 
 let check_one_lib admit senv (dir,m) =
   let md = m.library_compiled in
@@ -327,7 +337,6 @@ let intern_from_file ~intern_mode (dir, f) =
       let (sd:summary_disk), _, digest = marshal_in_segment f ch in
       let (md:library_disk), _, digest = marshal_in_segment f ch in
       let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in
-      let (discharging:'a option), _, _ = marshal_in_segment f ch in
       let (tasks:'a option), _, _ = marshal_in_segment f ch in
       let (table:seg_proofs option), pos, checksum =
         marshal_or_skip ~intern_mode f ch in
@@ -340,7 +349,7 @@ let intern_from_file ~intern_mode (dir, f) =
       if dir <> sd.md_name then
         user_err ~hdr:"intern_from_file"
           (name_clash_message dir sd.md_name f);
-      if tasks <> None || discharging <> None then
+      if tasks <> None then
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ccce0bd9a7..0684623a81 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -8,13 +8,13 @@ open Environ
 
 (** {6 Checking constants } *)
 
-let get_proof = ref (fun _ _ -> assert false)
-let set_indirect_accessor f = get_proof := f
-
-let indirect_accessor = {
-  Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
+let indirect_accessor = ref {
+  Opaqueproof.access_proof = (fun _ _ -> assert false);
+  Opaqueproof.access_discharge = (fun _ _ _ -> assert false);
 }
 
+let set_indirect_accessor f = indirect_accessor := f
+
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   (* Locally set the oracle for further typechecking *)
@@ -40,7 +40,7 @@ let check_constant_declaration env kn cb =
   let body = match cb.const_body with
   | Undef _ | Primitive _ -> None
   | Def c -> Some (Mod_subst.force_constr c)
-  | OpaqueDef o -> Some (Opaqueproof.force_proof indirect_accessor otab o)
+  | OpaqueDef o -> Some (Opaqueproof.force_proof !indirect_accessor otab o)
   in
   let () =
     match body with
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index dbc81c8507..7aa1f837a0 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -8,6 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit
+val set_indirect_accessor : Opaqueproof.indirect_accessor -> unit
 
 val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 031f05dd6b..4a4c8d803c 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -131,7 +131,7 @@ let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
 let rec v_constr =
   Sum ("constr",0,[|
     [|Int|]; (* Rel *)
-    [|Fail "Var"|]; (* Var *)
+    [|v_id|]; (* Var *)
     [|Fail "Meta"|]; (* Meta *)
     [|Fail "Evar"|]; (* Evar *)
     [|v_sort|]; (* Sort *)
@@ -383,6 +383,22 @@ let v_libsum =
 let v_lib =
   Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
 
-let v_opaques = Array (Opt v_constr)
+let v_ndecl = v_sum "named_declaration" 0
+    [| [|v_binder_annot v_id; v_constr|];               (* LocalAssum *)
+       [|v_binder_annot v_id; v_constr; v_constr|] |]   (* LocalDef *)
+
+let v_nctxt = List v_ndecl
+
+let v_work_list =
+  let v_abstr = v_pair v_instance (Array v_id) in
+  Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|])
+
+let v_abstract =
+  Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |])
+
+let v_cooking_info =
+  Tuple ("cooking_info", [|v_work_list; v_abstract|])
+
+let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt v_constr |]))
 let v_univopaques =
   Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 620efbafd6..1336e3e8bf 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -202,17 +202,21 @@ let lift_univs cb subst auctx0 =
     let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
     subst, (Polymorphic auctx)
 
-let cook_constr { Opaqueproof.modlist ; abstract } c =
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
-  (* For now the STM only handles deferred computation of monomorphic
-    constants. The API will need to be adapted when it's not the case
-    anymore. *)
-  let () = assert (AUContext.is_empty abs_ctx) in
+  let ainst = Instance.of_array (Array.init univs Level.var) in
+  let usubst = Instance.append usubst ainst in
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps = Context.Named.map expmod abstract in
   let hyps = abstract_context hyps in
-  abstract_constant_body (expmod c) hyps
+  let c = abstract_constant_body (expmod c) hyps in
+  univs + AUContext.size abs_ctx, c
+
+let cook_constr infos univs c =
+  let fold info (univs, c) = cook_constr info (univs, c) in
+  let (_, c) = List.fold_right fold infos (univs, c) in
+  c
 
 let cook_constant { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
@@ -227,7 +231,7 @@ let cook_constant { from = cb; info } =
   | Undef _ as x -> x
   | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
   | OpaqueDef o ->
-    OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:map info o)
+    OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
   | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
   let const_hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index abae3880d7..934b7c6b50 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -28,7 +28,7 @@ type 'opaque result = {
 }
 
 val cook_constant : recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info -> constr -> constr
+val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr
 
 val cook_inductive :
   Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 1971c67c61..e18b726111 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,19 +16,22 @@ open Mod_subst
 type work_list = (Instance.t * Id.t array) Cmap.t * 
   (Instance.t * Id.t array) Mindmap.t
 
+type cooking_info = {
+  modlist : work_list;
+  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
+  access_discharge : cooking_info list -> int -> constr -> constr;
 }
 
-type cooking_info = { 
-  modlist : work_list; 
-  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 type proofterm = (constr * Univ.ContextSet.t) Future.computation
+type universes = int
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
-  | Direct of cooking_info list * proofterm
+  | Direct of universes * cooking_info list * proofterm
 type opaquetab = {
-  opaque_val : (cooking_info list * proofterm) Int.Map.t;
+  opaque_val : (int * cooking_info list * proofterm) Int.Map.t;
   (** Actual proof terms *)
   opaque_len : int;
   (** Size of the above map *)
@@ -43,14 +46,14 @@ let empty_opaquetab = {
 let not_here () =
   CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
-let create cu = Direct ([],cu)
+let create ~univs cu = Direct (univs, [],cu)
 
 let turn_indirect dp o tab = match o with
   | Indirect (_,_,i) ->
       if not (Int.Map.mem i tab.opaque_val)
       then CErrors.anomaly (Pp.str "Indirect in a different table.")
       else CErrors.anomaly (Pp.str "Already an indirect opaque.")
-  | Direct (d,cu) ->
+  | Direct (nunivs, d, cu) ->
     (* Invariant: direct opaques only exist inside sections, we turn them
       indirect as soon as we are at toplevel. At this moment, we perform
       hashconsing of their contents, potentially as a future. *)
@@ -61,7 +64,7 @@ let turn_indirect dp o tab = match o with
       in
       let cu = Future.chain cu hcons in
       let id = tab.opaque_len in
-      let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
+      let opaque_val = Int.Map.add id (nunivs, d,cu) tab.opaque_val in
       let opaque_dir =
         if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
         else if DirPath.equal tab.opaque_dir DirPath.initial then dp
@@ -74,10 +77,10 @@ let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
   | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
 
-let discharge_direct_opaque ~cook_constr ci = function
+let discharge_direct_opaque ci = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-  | Direct (d,cu) ->
-      Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
+  | Direct (n, d, cu) ->
+      Direct (n, ci :: d, cu)
 
 let join except cu = match except with
 | None -> ignore (Future.join cu)
@@ -86,54 +89,61 @@ let join except cu = match except with
   else ignore (Future.join cu)
 
 let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> join except cu
+  | Direct (_,_,cu) -> join except cu
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp then
-        let fp = snd (Int.Map.find i prfs) in
+        let (_, _, fp) = Int.Map.find i prfs in
         join except fp
 
 let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) ->
-      fst(Future.force cu)
+  | Direct (n, d, cu) ->
+    let (c, _) = Future.force cu in
+    access.access_discharge d n c
   | Indirect (l,dp,i) ->
-      let pt =
+      let c =
         if DirPath.equal dp odp
-        then Future.chain (snd (Int.Map.find i prfs)) fst
+        then
+          let (n, d, cu) = Int.Map.find i prfs in
+          let (c, _) = Future.force cu in
+          access.access_discharge d n c
         else match access.access_proof dp i with
         | None -> not_here ()
-        | Some v -> Future.from_val v
+        | Some v -> v
       in
-      let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
 let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> snd(Future.force cu)
+  | Direct (_,_,cu) ->
+    snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
-      then snd (Future.force (snd (Int.Map.find i prfs)))
+      then
+        let (_, _, cu) = Int.Map.find i prfs in
+        snd (Future.force cu)
       else Univ.ContextSet.empty
 
 let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-| Direct (_, cu) -> Future.chain cu snd
+| Direct (_, _, cu) -> Future.chain cu snd
 
 module FMap = Future.UUIDMap
 
 let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
-  let opaque_table = Array.make n None in
-  let disch_table = Array.make n [] in
+  let opaque_table = Array.make n ([], 0, None) in
   let f2t_map = ref FMap.empty in
-  let iter n (d, cu) =
+  let iter n (univs, d, cu) =
     let uid = Future.uuid cu in
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
-    if Future.is_val cu then
-      let (c, _) = Future.force cu in
-      opaque_table.(n) <- Some c
-    else if Future.UUIDSet.mem uid except then
-      disch_table.(n) <- d
-    else
-      CErrors.anomaly
-        Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+    let c =
+      if Future.is_val cu then
+        let (c, _) = Future.force cu in
+        Some c
+      else if Future.UUIDSet.mem uid except then None
+      else
+        CErrors.anomaly
+          Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+    in
+    opaque_table.(n) <- (d, univs, c)
   in
   let () = Int.Map.iter iter otab in
-  opaque_table, disch_table, !f2t_map
+  opaque_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 46b0500507..6e275649cd 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -28,15 +28,23 @@ type opaque
 val empty_opaquetab : opaquetab
 
 (** From a [proofterm] to some [opaque]. *)
-val create : proofterm -> opaque
+val create : univs:int -> proofterm -> opaque
 
 (** Turn a direct [opaque] into an indirect one. It is your responsibility to
   hashcons the inner term beforehand. The integer is an hint of the maximum id
   used so far *)
 val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
+type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
+  (Univ.Instance.t * Id.t array) Mindmap.t
+
+type cooking_info = {
+  modlist : work_list;
+  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
+  access_discharge : cooking_info list -> int -> constr -> constr;
 }
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The two functions above activate
@@ -51,23 +59,11 @@ val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 
 val subst_opaque : substitution -> opaque -> opaque
 
-type work_list = (Univ.Instance.t * Id.t array) Cmap.t * 
-  (Univ.Instance.t * Id.t array) Mindmap.t
-
-type cooking_info = { 
-  modlist : work_list; 
-  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
-
-(* The type has two caveats:
-   1) cook_constr is defined after
-   2) we have to store the input in the [opaque] in order to be able to
-      discharge it when turning a .vi into a .vo *)
 val discharge_direct_opaque :
-  cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
+  cooking_info -> opaque -> opaque
 
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
-  Constr.t option array *
-  cooking_info list array *
+  (cooking_info list * int * Constr.t option) array *
   int Future.UUIDMap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9f7466902d..759cbe22ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -749,9 +749,13 @@ let export_side_effects mb env (b_ctx, eff) =
      in
        translate_seff trusted seff [] env
 
+let n_univs cb = match cb.const_universes with
+| Monomorphic _ -> 0
+| Polymorphic auctx -> Univ.AUContext.size auctx
+
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in
+  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val p)) cb) in
   let bodies = List.map map exported in
   let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -778,7 +782,7 @@ let add_constant ?role ~in_section l decl senv =
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
     in
   let senv =
-    let cb = map_constant Opaqueproof.create cb in
+    let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
diff --git a/library/library.ml b/library/library.ml
index e3b8511af1..1ac75d2fdc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -276,11 +276,11 @@ let in_import_library : DirPath.t list * bool -> obj =
 (** Delayed / available tables of opaque terms *)
 
 type 'a table_status =
-  | ToFetch of 'a option array delayed
-  | Fetched of 'a option array
+  | ToFetch of 'a array delayed
+  | Fetched of 'a array
 
 let opaque_tables =
-  ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
+  ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -306,10 +306,14 @@ let access_table what tables dp i =
 
 let access_opaque_table dp i =
   let what = "opaque proofs" in
-  access_table what opaque_tables dp i
+  let (info, n, c) = access_table what opaque_tables dp i in
+  match c with
+  | None -> None
+  | Some c -> Some (Cooking.cook_constr info n c)
 
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
+  Opaqueproof.access_discharge = Cooking.cook_constr;
 }
 
 (************************************************************************)
@@ -319,8 +323,7 @@ type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
   Univ.ContextSet.t * bool
-type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 let mk_library sd md digests univs =
   {
@@ -344,7 +347,6 @@ let intern_from_file f =
   let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
   let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
   let _ = System.skip_in_segment f ch in
-  let _ = System.skip_in_segment f ch in
   let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
   close_in ch;
   register_library_filename lsd.md_name f;
@@ -527,15 +529,13 @@ let load_library_todo f =
   let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
   let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
   let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
-  let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
   let tasks, _, _ = System.marshal_in_segment f ch in
-  let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
+  let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in
   close_in ch;
   if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
-  if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
-  s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
+  s0, s1, Option.get s2, Option.get tasks, s4
 
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -578,10 +578,10 @@ let save_library_to ?todo ~output_native_objects dir f otab =
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
   let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
-  let opaque_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
-  let tasks, utab, dtab =
+  let opaque_table, f2t_map = Opaqueproof.dump ~except otab in
+  let tasks, utab =
     match todo with
-    | None -> None, None, None
+    | None -> None, None
     | Some (tasks, rcbackup) ->
         let tasks =
           List.map Stateid.(fun (r,b) ->
@@ -589,8 +589,8 @@ let save_library_to ?todo ~output_native_objects dir f otab =
             with Not_found -> assert b; { r with uuid = -1 }, b)
           tasks in
         Some (tasks,rcbackup),
-        Some (Univ.ContextSet.empty,false),
-        Some disch_table in
+        Some (Univ.ContextSet.empty,false)
+  in
   let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
@@ -610,7 +610,6 @@ let save_library_to ?todo ~output_native_objects dir f otab =
     System.marshal_out_segment f' ch (sd           : seg_sum);
     System.marshal_out_segment f' ch (md           : seg_lib);
     System.marshal_out_segment f' ch (utab         : seg_univ option);
-    System.marshal_out_segment f' ch (dtab         : seg_discharge option);
     System.marshal_out_segment f' ch (tasks        : 'tasks option);
     System.marshal_out_segment f' ch (opaque_table : seg_proofs);
     close_out ch;
@@ -630,7 +629,6 @@ let save_library_raw f sum lib univs proofs =
   System.marshal_out_segment f ch (sum        : seg_sum);
   System.marshal_out_segment f ch (lib        : seg_lib);
   System.marshal_out_segment f ch (Some univs : seg_univ option);
-  System.marshal_out_segment f ch (None       : seg_discharge option);
   System.marshal_out_segment f ch (None       : 'tasks option);
   System.marshal_out_segment f ch (proofs     : seg_proofs);
   close_out ch
diff --git a/library/library.mli b/library/library.mli
index 142206e2c5..727eca10cf 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -35,8 +35,7 @@ type seg_sum
 type seg_lib
 type seg_univ = (* all_cst, finished? *)
   Univ.ContextSet.t * bool
-type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
@@ -51,7 +50,7 @@ val save_library_to :
 
 val load_library_todo
   :  CUnix.physical_path
-  -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+  -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs
 
 val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 0efea0b8e0..5baa6ce251 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1639,7 +1639,7 @@ and Slaves : sig
   val info_tasks : 'a tasks -> (string * float * int) list
   val finish_task :
     string ->
-    Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+    Library.seg_univ -> Library.seg_proofs ->
     int tasks -> int -> Library.seg_univ
 
   val cancel_worker : WorkerPool.worker_id -> unit
@@ -1724,7 +1724,7 @@ end = struct (* {{{ *)
                       str (Printexc.to_string e)));
       if drop then `ERROR_ADMITTED else `ERROR
 
-  let finish_task name (cst,_) d p l i =
+  let finish_task name (cst,_) p l i =
     let { Stateid.uuid = bucket }, drop = List.nth l i in
     let bucket_name =
       if bucket < 0 then (assert drop; ", no bucket")
@@ -1734,7 +1734,6 @@ end = struct (* {{{ *)
     | `ERROR_ADMITTED -> cst, false
     | `OK_ADMITTED -> cst, false
     | `OK (po,_) ->
-        let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
         let con =
           Nametab.locate_constant
             (Libnames.qualid_of_ident po.Proof_global.id) in
@@ -1746,12 +1745,14 @@ end = struct (* {{{ *)
            the call to [check_task_aux] above. *)
         let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in
         let uc = Univ.hcons_universe_context_set uc in
+        let (pr, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in
         (* We only manipulate monomorphic terms here. *)
-        let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
-        let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in
-        let pr = discharge pr in
+        let () = assert (Univ.AUContext.is_empty ctx) in
         let pr = Constr.hcons pr in
-        p.(bucket) <- Some pr;
+        let (ci, univs, dummy) = p.(bucket) in
+        let () = assert (Option.is_empty dummy) in
+        let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in
+        p.(bucket) <- ci, univs, Some pr;
         Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
@@ -2747,11 +2748,11 @@ let check_task name (tasks,rcbackup) i =
   with e when CErrors.noncritical e -> VCS.restore vcs; false
 let info_tasks (tasks,_) = Slaves.info_tasks tasks
 
-let finish_tasks name u d p (t,rcbackup as tasks) =
+let finish_tasks name u p (t,rcbackup as tasks) =
   RemoteCounter.restore rcbackup;
   let finish_task u (_,_,i) =
     let vcs = VCS.backup () in
-    let u = State.purify (Slaves.finish_task name u d p t) i in
+    let u = State.purify (Slaves.finish_task name u p t) i in
     VCS.restore vcs;
     u in
   try
diff --git a/stm/stm.mli b/stm/stm.mli
index 5e1e9bf5ad..86e2566539 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -167,7 +167,7 @@ type tasks
 val check_task : string -> tasks -> int -> bool
 val info_tasks : tasks -> (string * float * int) list
 val finish_tasks : string ->
-  Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+  Library.seg_univ -> Library.seg_proofs ->
     tasks -> Library.seg_univ * Library.seg_proofs
 
 (* Id of the tip of the current branch *)
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 0f78e0acf6..cf0c8934b0 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -12,7 +12,7 @@ open Util
 
 let check_vio (ts,f_in) =
   Dumpglob.noglob ();
-  let _, _, _, _, tasks, _ = Library.load_library_todo f_in in
+  let _, _, _, tasks, _ = Library.load_library_todo f_in in
   Stm.set_compilation_hints f_in;
   List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts
 
@@ -29,7 +29,7 @@ let schedule_vio_checking j fs =
   if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
   let jobs = ref [] in
   List.iter (fun long_f_dot_vio ->
-    let _,_,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in
+    let _,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in
     Stm.set_compilation_hints long_f_dot_vio;
     let infos = Stm.info_tasks tasks in
     let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 7748134146..2e25066897 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -176,9 +176,9 @@ let compile opts copts ~echo ~f_in ~f_out =
       Dumpglob.noglob ();
       let long_f_dot_vio, long_f_dot_vo =
         ensure_exists_with_prefix f_in f_out ".vio" ".vo" in
-      let sum, lib, univs, disch, tasks, proofs =
+      let sum, lib, univs, tasks, proofs =
         Library.load_library_todo long_f_dot_vio in
-      let univs, proofs = Stm.finish_tasks long_f_dot_vo univs disch proofs tasks in
+      let univs, proofs = Stm.finish_tasks long_f_dot_vo univs proofs tasks in
       Library.save_library_raw long_f_dot_vo sum lib univs proofs
 
 let compile opts copts ~echo ~f_in ~f_out =