From 0f54a91eac98baf076d8be8f52bccdb1de17ea46 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jun 2019 10:19:02 +0200
Subject: Slightly tweak the representation of dischargeable opaque proofs.

This will allow an easier removal of the discharge segment in a later
commit.
---
 kernel/opaqueproof.ml  | 4 ++--
 kernel/opaqueproof.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3