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.
---
 library/library.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/library.mli')

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