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.

1 files changed, 1 insertions, 1 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 6aecc368e6..56b7a16ace 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -533,7 +533,7 @@ let emit_side_effects eff u =
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = UnivGen.new_univ_level () in
+  let u = UnivGen.fresh_level () in
   let ctx' = Univ.ContextSet.add_universe u ctx in
   let uctx', pred =
     match rigid with