checker: Change in library on disk values, now using context_sets instead of

constraints only.

4 files changed, 21 insertions, 3 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 6ed9a4d25..12146715a 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -433,7 +433,7 @@ type library_disk = {
 
 type opaque_table = constr Future.computation array
 type univ_table =
-  (Univ.constraints Future.computation array * Univ.constraints * bool) option
+  (Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool) option
 
 (** A .vo file is currently made of :
 
diff --git a/checker/univ.ml b/checker/univ.ml
index 323a373ec..cb530149b 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -379,7 +379,8 @@ module Level = struct
 
 end
 
-(** Level maps *)
+(** Level sets and maps *)
+module LSet = Set.Make (Level)
 module LMap = Map.Make (Level)
 
 type 'a universe_map = 'a LMap.t
@@ -1297,6 +1298,14 @@ end
 
 type universe_context = UContext.t
 
+module ContextSet =
+struct
+  type t = LSet.t constrained
+  let empty = LSet.empty, Constraint.empty
+  let constraints (_, cst) = cst
+end
+type universe_context_set = ContextSet.t
+
 (** Substitutions. *)
 
 let is_empty_subst = LMap.is_empty
diff --git a/checker/univ.mli b/checker/univ.mli
index 89dd64486..a4a3a9cb1 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -188,7 +188,15 @@ sig
 
 end
 
+module ContextSet :
+  sig 
+    type t
+    val empty : t
+    val constraints : t -> constraints
+  end
+
 type universe_context = UContext.t
+type universe_context_set = ContextSet.t
 
 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
diff --git a/checker/values.ml b/checker/values.ml
index f55cf63fc..4a4f5a190 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 *)