From 7ebe6117789ac3c0d31c8a6ed918fce71b6d2e4b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Dec 2014 20:22:37 +0100
Subject: checker: Change in library on disk values, now using context_sets
 instead of constraints only.

---
 checker/values.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'checker/values.ml')

diff --git a/checker/values.ml b/checker/values.ml
index f55cf63fcf..4a4f5a1905 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -111,6 +111,7 @@ let v_cstrs =
 
 let v_instance = Annot ("instance", Array v_level)
 let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
+let v_context_set = v_tuple "universe_context_set" [|v_set v_level;v_cstrs|]
 
 (** kernel/term *)
 
@@ -328,7 +329,7 @@ let v_lib =
 
 let v_opaques = Array (v_computation v_constr)
 let v_univopaques =
-  Opt (Tuple ("univopaques",[|Array (v_computation v_cstrs);v_cstrs;v_bool|]))
+  Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
 
 (** Registering dynamic values *)
 
-- 
cgit v1.2.3