From 3e275d4bd1c3eb002b68c36ab116e5ab687d52f3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 4 Dec 2018 10:33:47 +0100
Subject: Fix race condition triggered by fresh universe generation

Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
---
 checker/values.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/values.ml b/checker/values.ml
index dcb2bca81a..f73e19a972 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -93,9 +93,9 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|]
 
 
 (** kernel/univ *)
-
+let v_level_qualid = v_tuple "Level.Qualid.t" [|v_dp;Int|]
 let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) 
-  [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|]
+  [|(*Level*)[|v_level_qualid|]; (*Var*)[|Int|]|]
 let v_level = v_tuple "level" [|Int;v_raw_level|] 
 let v_expr = v_tuple "levelexpr" [|v_level;Int|]
 let v_univ = List v_expr
-- 
cgit v1.2.3