2 files changed, 8 insertions, 8 deletions
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 *)