Merge PR #14050: Remove remote counter system

Reviewed-by: gares
Ack-by: ppedrot
Ack-by: ejgallego

20 files changed, 134 insertions, 169 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/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh
new file mode 100644
index 0000000000..d1606711dc
--- /dev/null
+++ b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh
@@ -0,0 +1 @@
+overlay metacoq https://github.com/SkySkimmer/metacoq no-remote-counter-alt 14050
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 278ca6bf34..b917d91512 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,14 +13,14 @@ open Names
 open Constr
 open Univ
 
-type univ_unique_id = int
 (* Generator of levels *)
-let new_univ_id, set_remote_new_univ_id =
-  RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> n)
+let new_univ_id =
+  let cnt = ref 0 in
+  fun () -> incr cnt; !cnt
 
 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/engine/univGen.mli b/engine/univGen.mli
index 05737411f5..743d819747 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -13,12 +13,6 @@ open Constr
 open Environ
 open Univ
 
-
-(** The global universe counter *)
-type univ_unique_id
-val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer
-val new_univ_id : unit -> univ_unique_id (** for the stm *)
-
 (** Side-effecting functions creating new universe levels. *)
 
 val new_univ_global : unit -> Level.UGlobal.t
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/lib/remoteCounter.ml b/lib/remoteCounter.ml
deleted file mode 100644
index 9ea751eef9..0000000000
--- a/lib/remoteCounter.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-type 'a getter = unit -> 'a
-type 'a installer = ('a getter) -> unit
-
-type remote_counters_status = (string * Obj.t) list
-
-let counters : remote_counters_status ref = ref []
-
-let (!!) x = !(!x)
-
-let new_counter ~name a ~incr ~build =
-  assert(not (List.mem_assoc name !counters));
-  let data = ref (ref a) in
-  counters := (name, Obj.repr data) :: !counters;
-  let m = Mutex.create () in
-  let mk_thsafe_local_getter f () =
-    (* - slaves must use a remote counter getter, not this one! *)
-    (* - in the main process there is a race condition between slave
-         managers (that are threads) and the main thread, hence the mutex *)
-    if Flags.async_proofs_is_worker () then
-      CErrors.anomaly(Pp.str"Slave processes must install remote counters.");
-    let x = CThread.with_lock m ~scope:f in
-    build x in
-  let mk_thsafe_remote_getter f () =
-    CThread.with_lock m ~scope:f in
-  let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in
-  let installer f =
-    if not (Flags.async_proofs_is_worker ()) then
-      CErrors.anomaly(Pp.str"Only slave processes can install a remote counter.");
-    getter := mk_thsafe_remote_getter f in
-  (fun () -> !getter ()), installer
-
-let backup () = !counters
-
-let snapshot () =
-  List.map (fun (n,v) -> n, Obj.repr (ref (ref !!(Obj.obj v)))) !counters
-
-let restore l =
-  List.iter (fun (name, data) ->
-    assert(List.mem_assoc name !counters);
-    let dataref = Obj.obj (List.assoc name !counters) in
-    !dataref := !!(Obj.obj data))
-  l
diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli
deleted file mode 100644
index 42d1f8a8d1..0000000000
--- a/lib/remoteCounter.mli
+++ /dev/null
@@ -1,31 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Remote counters are *global* counters for fresh ids.  In the master/slave
- * scenario, the slave installs a getter that asks the master for a fresh
- * value.  In the scenario of a slave that runs after the death of the master
- * on some marshalled data, a backup of all counters status should be taken and
- * restored to avoid reusing ids.
- * Counters cannot be created by threads, they must be created once and forall
- * as toplevel module declarations. *)
-
-
-type 'a getter = unit -> 'a
-type 'a installer = ('a getter) -> unit
-
-val new_counter : name:string ->
-  'a -> incr:('a -> 'a) -> build:('a -> 'b) -> 'b getter * 'b installer
-
-type remote_counters_status
-val backup : unit -> remote_counters_status
-(* like backup but makes a copy so that further increment does not alter
- * the snapshot *)
-val snapshot : unit -> remote_counters_status
-val restore : remote_counters_status -> unit
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index dd80ff21aa..a9f203014f 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -56,12 +56,8 @@ module Make(T : Task) () = struct
   type response =
     | Response of T.response
     | RespFeedback of Feedback.feedback
-    | RespGetCounterNewUnivLevel
   type request = Request of T.request
 
-  type more_data =
-    | MoreDataUnivLevel of UnivGen.univ_unique_id list
-
   let slave_respond (Request r) =
     let res = T.perform r in
     Response res
@@ -94,16 +90,6 @@ module Make(T : Task) () = struct
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("unmarshal_response: "^s)
 
-  let marshal_more_data oc (res : more_data) =
-    try marshal_to_channel oc res
-    with Failure s | Invalid_argument s | Sys_error s ->
-      marshal_err ("marshal_more_data: "^s)
-
-  let unmarshal_more_data ic =
-    try (CThread.thread_friendly_input_value ic : more_data)
-    with Failure s | Invalid_argument s | Sys_error s ->
-      marshal_err ("unmarshal_more_data: "^s)
-
   let report_status ?(id = !Flags.async_proofs_worker_id) s =
     let open Feedback in
     feedback ~id:Stateid.initial (WorkerStatus(id, s))
@@ -198,8 +184,6 @@ module Make(T : Task) () = struct
         | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i
         | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno
         | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in
-    let more_univs n =
-      CList.init n (fun _ -> UnivGen.new_univ_id ()) in
 
     let rec kill_if () =
       if not (Worker.is_alive proc) then ()
@@ -231,9 +215,6 @@ module Make(T : Task) () = struct
         marshal_request oc (Request req);
         let rec continue () =
           match unmarshal_response ic with
-          | RespGetCounterNewUnivLevel ->
-              marshal_more_data oc (MoreDataUnivLevel (more_univs 10));
-              continue ()
           | RespFeedback fbk -> T.forward_feedback fbk; continue ()
           | Response resp ->
               match T.use_response !worker_age task resp with
@@ -315,13 +296,6 @@ module Make(T : Task) () = struct
     let ic, oc = Spawned.get_channels () in
     slave_oc := Some oc; slave_ic := Some ic
 
-  let bufferize f =
-    let l = ref [] in
-    fun () ->
-      match !l with
-      | [] -> let data = f () in l := List.tl data; List.hd data
-      | x::tl -> l := tl; x
-
   let slave_handshake () =
     Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
 
@@ -339,11 +313,6 @@ module Make(T : Task) () = struct
           Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc) ()
     in
     ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x));
-    (* We ask master to allocate universe identifiers *)
-    UnivGen.set_remote_new_univ_id (bufferize @@ Control.protect_sigalrm (fun () ->
-      marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
-      match unmarshal_more_data (Option.get !slave_ic) with
-      | MoreDataUnivLevel l -> l));
     let working = ref false in
     slave_handshake ();
     while true do
diff --git a/stm/stm.ml b/stm/stm.ml
index f5768726c3..6287943cee 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2447,24 +2447,21 @@ let join ~doc =
   VCS.print ();
   doc
 
-let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot ()
-
-type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status
-let check_task name (tasks,rcbackup) i =
-  RemoteCounter.restore rcbackup;
+type tasks = int Slaves.tasks
+let check_task name tasks i =
   let vcs = VCS.backup () in
   try
     let rc = State.purify (Slaves.check_task name tasks) i in
     VCS.restore vcs;
     rc
   with e when CErrors.noncritical e -> VCS.restore vcs; false
-let info_tasks (tasks,_) = Slaves.info_tasks tasks
 
-let finish_tasks name u p (t,rcbackup as tasks) =
-  RemoteCounter.restore rcbackup;
+let info_tasks = Slaves.info_tasks
+
+let finish_tasks name u p tasks =
   let finish_task u (_,_,i) =
     let vcs = VCS.backup () in
-    let u = State.purify (Slaves.finish_task name u p t) i in
+    let u = State.purify (Slaves.finish_task name u p tasks) i in
     VCS.restore vcs;
     u in
   try
@@ -2515,13 +2512,13 @@ let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo =
     CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
   (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers,
   below, [snapshot] gets computed even if [create_vos] is true. *)
-  let (tasks,counters) = dump_snapshot() in
+  let tasks = Slaves.dump_snapshot() in
   let except = List.fold_left (fun e (r,_) ->
      Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in
   let todo_proofs =
     if create_vos
       then Library.ProofsTodoSomeEmpty except
-      else Library.ProofsTodoSome (except,tasks,counters)
+      else Library.ProofsTodoSome (except,tasks)
     in
   Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
   doc
diff --git a/test-suite/misc/vio_checking.sh b/test-suite/misc/vio_checking.sh
new file mode 100755
index 0000000000..ffa909e93b
--- /dev/null
+++ b/test-suite/misc/vio_checking.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+set -ex
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc
+
+rm -f vio_checking{,bad}.{vo,vio}
+
+coqc -vio vio_checking.v
+coqc -vio vio_checking_bad.v
+
+coqc -schedule-vio-checking 2 vio_checking.vio
+
+if coqc -schedule-vio-checking 2 vio_checking_bad.vio; then
+    echo 'vio-checking on vio_checking_bad.vio should have failed!'
+    exit 1
+fi
+if coqc -schedule-vio-checking 2 vio_checking.vio vio_checking_bad.vio; then
+    echo 'vio-checking on vio_checking vio_checking_bad.vio should have failed!'
+    exit 1
+fi
+
+coqc -vio2vo vio_checking.vio
+coqchk -silent vio_checking.vo
+
+if coqc -vio2vo vio_checking_bad.vio; then
+    echo 'vio2vo on vio_checking_bad.vio should have failed!'
+    exit 1
+fi
diff --git a/test-suite/misc/vio_checking.v b/test-suite/misc/vio_checking.v
new file mode 100644
index 0000000000..8dd5e47383
--- /dev/null
+++ b/test-suite/misc/vio_checking.v
@@ -0,0 +1,9 @@
+
+Lemma foo : Type.
+Proof. exact Type. Qed.
+
+Lemma foo1 : Type.
+Proof. exact Type. Qed.
+
+Lemma foo2 : Type.
+Proof. exact foo1. Qed.
diff --git a/test-suite/misc/vio_checking_bad.v b/test-suite/misc/vio_checking_bad.v
new file mode 100644
index 0000000000..f32d06f34a
--- /dev/null
+++ b/test-suite/misc/vio_checking_bad.v
@@ -0,0 +1,4 @@
+(* a file to check that vio-checking is not a noop *)
+
+Lemma foo : Type.
+Proof. match goal with |- ?G => exact G end. Qed.
diff --git a/test-suite/success/RemoteUnivs.v b/test-suite/success/RemoteUnivs.v
new file mode 100644
index 0000000000..5ab4937dda
--- /dev/null
+++ b/test-suite/success/RemoteUnivs.v
@@ -0,0 +1,31 @@
+
+
+Goal Type * Type.
+Proof.
+  split.
+  par: exact Type.
+Qed.
+
+Goal Type.
+Proof.
+  exact Type.
+Qed.
+
+(* (* coqide test, note the delegated proofs seem to get an empty dirpath?
+      or I got confused because I had lemma foo in file foo
+ *)
+Definition U := Type.
+
+Lemma foo : U.
+Proof.
+  exact Type.
+Qed.
+
+
+Lemma foo1 : Type.
+Proof.
+  exact (U:Type).
+Qed.
+
+Print foo.
+*)
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..df6f04792e 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
@@ -223,6 +223,7 @@ let compile_file opts stm_opts copts injections =
 (* VIO Dispatching                                                            *)
 (******************************************************************************)
 let check_vio_tasks copts =
+  Flags.async_proofs_worker_id := "VioChecking";
   let rc =
     List.fold_left (fun acc (n,f) ->
         let f_in = ensure ".vio" f f in
diff --git a/vernac/library.ml b/vernac/library.ml
index cc9e3c3c44..eedf8aa670 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -448,10 +448,10 @@ let save_library_base f sum lib univs tasks proofs =
     Sys.remove f;
     Exninfo.iraise reraise
 
-type ('document,'counters) todo_proofs =
+type 'document todo_proofs =
  | ProofsTodoNone (* for .vo *)
  | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *)
- | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *)
+ | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *)
 
 let save_library_to todo_proofs ~output_native_objects dir f otab =
   assert(
@@ -464,7 +464,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
   let except = match todo_proofs with
     | ProofsTodoNone -> Future.UUIDSet.empty
     | ProofsTodoSomeEmpty except -> except
-    | ProofsTodoSome (except,l,_) -> except
+    | ProofsTodoSome (except,l) -> except
     in
   let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
   let opaque_table, f2t_map = Opaqueproof.dump ~except otab in
@@ -473,13 +473,13 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
     | ProofsTodoNone -> None, None
     | ProofsTodoSomeEmpty _except ->
       None, Some (Univ.ContextSet.empty,false)
-    | ProofsTodoSome (_except, tasks, rcbackup) ->
+    | ProofsTodoSome (_except, tasks) ->
       let tasks =
         List.map Stateid.(fun (r,b) ->
             try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b
             with Not_found -> assert b; { r with uuid = -1 }, b)
           tasks in
-      Some (tasks,rcbackup),
+      Some tasks,
       Some (Univ.ContextSet.empty,false)
     in
     let sd = {
diff --git a/vernac/library.mli b/vernac/library.mli
index d0e9f84691..4c6c654c58 100644
--- a/vernac/library.mli
+++ b/vernac/library.mli
@@ -41,13 +41,13 @@ type seg_proofs = Opaqueproof.opaque_proofterm array
     argument.
     [output_native_objects]: when producing vo objects, also compile the native-code version. *)
 
-type ('document,'counters) todo_proofs =
+type 'document todo_proofs =
  | ProofsTodoNone (* for .vo *)
  | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *)
- | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *)
+ | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *)
 
 val save_library_to :
-  ('document,'counters) todo_proofs ->
+  'document todo_proofs ->
   output_native_objects:bool ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
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 =