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

(limited to 'checker/values.ml')

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