Slightly tweak the representation of dischargeable opaque proofs.

This will allow an easier removal of the discharge segment in a later
commit.

7 files changed, 17 insertions, 16 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 747d7c43a1..030b605e3f 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 = (Opaqueproof.cooking_info list * int * 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,10 @@ let access_opaque_table dp i =
     with Not_found -> assert false
   in
   assert (i < Array.length t);
-  match t.(i) with
+  let (info, n, c) = t.(i) in
+  match c with
   | None -> None
-  | Some (info, n, c) -> Some (Cooking.cook_constr info n c)
+  | Some c -> Some (Cooking.cook_constr info n c)
 
 let access_discharge = Cooking.cook_constr
 
diff --git a/checker/values.ml b/checker/values.ml
index 6dbf281f49..4a4c8d803c 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -399,6 +399,6 @@ let v_abstract =
 let v_cooking_info =
   Tuple ("cooking_info", [|v_work_list; v_abstract|])
 
-let v_opaques = Array (Opt (Tuple ("opaque", [| List v_cooking_info; Int; v_constr |])))
+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/opaqueproof.ml b/kernel/opaqueproof.ml
index ee549dee4f..02d8ff0672 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -129,7 +129,7 @@ let get_direct_constraints = function
 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 opaque_table = Array.make n ([], 0, None) in
   let disch_table = Array.make n [] in
   let f2t_map = ref FMap.empty in
   let iter n (univs, d, cu) =
@@ -137,7 +137,7 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
     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 (d, univs, c)
+      opaque_table.(n) <- (d, univs, Some c)
     else if Future.UUIDSet.mem uid except then
       (* Only monomorphic constraints can be delayed currently *)
       let () = assert (Int.equal univs 0) in
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 47439a787d..41f5ebb6b3 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -65,6 +65,6 @@ val discharge_direct_opaque :
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
-  (cooking_info list * int * Constr.t) option array *
+  (cooking_info list * int * Constr.t option) array *
   cooking_info list array *
   int Future.UUIDMap.t
diff --git a/library/library.ml b/library/library.ml
index 0a57a85c35..8030b835be 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 : ((Opaqueproof.cooking_info list * int * 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,10 @@ let access_table what tables dp i =
 
 let access_opaque_table dp i =
   let what = "opaque proofs" in
-  let ans = access_table what opaque_tables dp i in
-  match ans with
+  let (info, n, c) = access_table what opaque_tables dp i in
+  match c with
   | None -> None
-  | Some (info, n, c) -> Some (Cooking.cook_constr info n c)
+  | Some c -> Some (Cooking.cook_constr info n c)
 
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
@@ -324,7 +324,7 @@ 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 = (Opaqueproof.cooking_info list * int * Constr.t) option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 let mk_library sd md digests univs =
   {
diff --git a/library/library.mli b/library/library.mli
index 0c5d6e33c1..284c66db5b 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -36,7 +36,7 @@ type seg_lib
 type seg_univ = (* all_cst, finished? *)
   Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t) 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 *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 8efb606ddc..ad18245dec 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1747,7 +1747,7 @@ end = struct (* {{{ *)
         (* We only manipulate monomorphic terms here. *)
         let () = assert (Univ.AUContext.is_empty ctx) in
         let pr = Constr.hcons pr in
-        p.(bucket) <- Some (d.(bucket), Univ.AUContext.size ctx, pr);
+        p.(bucket) <- d.(bucket), Univ.AUContext.size ctx, Some pr;
         Univ.ContextSet.union cst uc, false
 
   let check_task name l i =