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

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

3 files changed, 13 insertions, 12 deletions

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