Merge PR #10258: Remove the delayed universe table from object files.

Reviewed-by: SkySkimmer
Reviewed-by: gares

3 files changed, 5 insertions, 10 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 76f40dbac2..c5bc59e72a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -50,6 +50,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 library_t = {
@@ -90,7 +91,6 @@ let register_loaded_library m =
 
 (* Map from library names to table of opaque terms *)
 let opaque_tables = ref LibraryMap.empty
-let opaque_univ_tables = ref LibraryMap.empty
 
 let access_opaque_table dp i =
   let t =
@@ -326,7 +326,7 @@ let intern_from_file ~intern_mode (dir, f) =
       let ch = System.with_magic_number_check raw_intern_library f in
       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:'a option), _, udg = 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 =
@@ -345,7 +345,7 @@ let intern_from_file ~intern_mode (dir, f) =
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
        Flags.if_verbose chk_pp (str " (was a vio file) ");
-      Option.iter (fun (_,_,b) -> if not b then
+      Option.iter (fun (_,b) -> if not b then
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
         opaque_csts;
@@ -363,13 +363,9 @@ let intern_from_file ~intern_mode (dir, f) =
     with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
   Option.iter (fun table -> opaque_tables := LibraryMap.add sd.md_name table !opaque_tables) table;
-  Option.iter (fun (opaque_csts,_,_) ->
-    opaque_univ_tables :=
-      LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
-    opaque_csts;
   let extra_cst =
     Option.default Univ.ContextSet.empty
-      (Option.map (fun (_,cs,_) -> cs) opaque_csts) in
+      (Option.map (fun (cs,_) -> cs) opaque_csts) in
   mk_library sd md f table digest extra_cst
 
 let get_deps (dir, f) =
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1cf07e7cc7..1bc5891517 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -13,7 +13,6 @@ let set_indirect_accessor f = get_proof := f
 
 let indirect_accessor = {
   Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
-  Opaqueproof.access_constraints = (fun _ _ -> assert false);
 }
 
 let check_constant_declaration env kn cb =
diff --git a/checker/values.ml b/checker/values.ml
index adee9b8bde..031f05dd6b 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -385,4 +385,4 @@ let v_lib =
 
 let v_opaques = Array (Opt v_constr)
 let v_univopaques =
-  Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|]))
+  Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))