Put async worker id in universe names

This removes the need for the remote counter.

8 files changed, 37 insertions, 26 deletions

diff --git a/checker/values.ml b/checker/values.ml
index f7a367b986..1353435181 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -87,7 +87,7 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|]
 
 
 (** kernel/univ *)
-let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|]
+let v_level_global = v_tuple "Level.Global.t" [|v_dp;String;Int|]
 let v_raw_level = v_sum "raw_level" 3 (* SProp, Prop, Set *)
   [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|]
 let v_level = v_tuple "level" [|Int;v_raw_level|]
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 278ca6bf34..b98c15f245 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -20,7 +20,8 @@ let new_univ_id, set_remote_new_univ_id =
     ~build:(fun n -> n)
 
 let new_univ_global () =
-  Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
+  let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in
+  Univ.Level.UGlobal.make (Global.current_dirpath ()) s (new_univ_id ())
 
 let fresh_level () =
   Univ.Level.make (new_univ_global ())
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 6cb61174d3..ddbd5fa0a7 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -717,7 +717,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
      ienv_decompose_prod ienv' (n-1) b
      | _ -> assert false
 
-let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0))
+let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) "" 0))
 let dummy_implicit_sort = mkType (Universe.make dummy_univ)
 let lambda_implicit_lift n a =
   let anon = Context.make_annot Anonymous Sorts.Relevant in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index a2fd14025e..c2496f10b0 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -38,20 +38,22 @@ struct
   open Names
 
   module UGlobal = struct
-    type t = DirPath.t * int
+    type t = DirPath.t * string * int
 
-    let make dp i = (DirPath.hcons dp,i)
+    let make dp s i = (DirPath.hcons dp,s,i)
 
     let repr x : t = x
 
-    let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+    let equal (d, s, i) (d', s', i') = Int.equal i i' && DirPath.equal d d' && String.equal s s'
 
-    let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d)
+    let hash (d,s,i) = Hashset.Combine.combine3 i (String.hash s) (DirPath.hash d)
 
-    let compare (d, i) (d', i') =
-      let c = Int.compare i i' in
-      if Int.equal c 0 then DirPath.compare d d'
-      else c
+    let compare (d, s, i) (d', s', i') =
+      if i < i' then -1
+      else if i' < i then 1
+      else let c = DirPath.compare d d' in
+        if not (Int.equal c 0) then c
+        else String.compare s s'
   end
 
   type t =
@@ -84,10 +86,7 @@ struct
     | Set, Set -> 0
     | Set, _ -> -1
     | _, Set -> 1
-    | Level (dp1, i1), Level (dp2, i2) ->
-      if i1 < i2 then -1
-      else if i1 > i2 then 1
-      else DirPath.compare dp1 dp2
+    | Level l1, Level l2 -> UGlobal.compare l1 l2
     | Level _, _ -> -1
     | _, Level _ -> 1
     | Var n, Var m -> Int.compare n m
@@ -98,8 +97,8 @@ struct
       | SProp, SProp -> true
       | Prop, Prop -> true
       | Set, Set -> true
-      | Level (n,d), Level (n',d') ->
-        n == n' && d == d'
+      | Level (d,s,n), Level (d',s',n') ->
+        n == n' && s==s' && d == d'
       | Var n, Var n' -> n == n'
       | _ -> false
 
@@ -107,9 +106,10 @@ struct
     | SProp as x -> x
     | Prop as x -> x
     | Set as x -> x
-    | Level (d,n) as x ->
+    | Level (d,s,n) as x ->
+      let s' = CString.hcons s in
       let d' = Names.DirPath.hcons d in
-        if d' == d then x else Level (d',n)
+        if s' == s && d' == d then x else Level (d',s',n)
     | Var _n as x -> x
 
   open Hashset.Combine
@@ -119,7 +119,7 @@ struct
     | Prop -> combinesmall 1 1
     | Set -> combinesmall 1 2
     | Var n -> combinesmall 2 n
-    | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d))
+    | Level l -> combinesmall 3 (UGlobal.hash l)
 
 end
 
@@ -200,7 +200,10 @@ module Level = struct
     | SProp -> "SProp"
     | Prop -> "Prop"
     | Set -> "Set"
-    | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n
+    | Level (d,s,n) ->
+      Names.DirPath.to_string d ^
+      (if CString.is_empty s then "" else "." ^ s) ^
+      "." ^ string_of_int n
     | Var n -> "Var(" ^ string_of_int n ^ ")"
 
   let pr u = str (to_string u)
@@ -218,7 +221,7 @@ module Level = struct
 
   let name u =
     match data u with
-    | Level (d, n) -> Some (d, n)
+    | Level l -> Some l
     | _ -> None
 end
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7286fc84cb..eeaa1ad62d 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -15,8 +15,8 @@ sig
   module UGlobal : sig
     type t
 
-    val make : Names.DirPath.t -> int -> t
-    val repr : t -> Names.DirPath.t * int
+    val make : Names.DirPath.t -> string -> int -> t
+    val repr : t -> Names.DirPath.t * string * int
     val equal : t -> t -> bool
     val hash : t -> int
     val compare : t -> t -> int
diff --git a/test-suite/vio/univ_constraints_statements_body.v b/test-suite/vio/univ_constraints_statements_body.v
new file mode 100644
index 0000000000..6302adefc2
--- /dev/null
+++ b/test-suite/vio/univ_constraints_statements_body.v
@@ -0,0 +1,7 @@
+Definition T := Type.
+Definition T1 : T := Type.
+
+Lemma x : True.
+Proof.
+exact (let a : T := Type in I).
+Qed.
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 041097d2d3..46651d1d8b 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -194,7 +194,7 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out =
       if mode = BuildVio then dump_empty_vos()
 
   | Vio2Vo ->
-
+      Flags.async_proofs_worker_id := "Vio2Vo";
       let sum, lib, univs, tasks, proofs =
         Library.load_library_todo long_f_dot_in in
       let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index af40292f18..54f034c74e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -413,7 +413,7 @@ let sort_universes g =
   let levels = traverse LMap.empty [normalize Level.set, 0] in
   let max_level = LMap.fold (fun _ n accu -> max n accu) levels 0 in
   let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in
-  let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp i))) in
+  let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp "" i))) in
   let ulevels = Array.cons Level.set ulevels in
   (* Add the normal universes *)
   let fold (cur, ans) u =