7 files changed, 5 insertions, 49 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 20ea24dd87..81559778f2 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -296,9 +296,6 @@ let add_constraints uctx cstrs =
     universes = UGraph.merge_constraints cstrs' uctx.universes;
     weak_constraints = weak; }
 
-(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
-(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)
-
 let add_universe_constraints uctx cstrs =
   let univs, local = uctx.local in
   let vars, weak, local' = process_universe_constraints uctx cstrs in
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/engine/univMinim.ml b/engine/univMinim.ml
index 4ed6e97526..86bf2c9298 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -406,6 +406,3 @@ let normalize_context_set ~lbound g ctx us algs weak =
   in
   let us = normalize_opt_subst us in
     (us, algs), (ctx', Constraint.union noneqs eqs)
-
-(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
-(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 8d6689933c..10ee601f3f 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Univ
-open UnivSubst
 
 type t =
   | ULe of Universe.t * Universe.t
@@ -22,24 +21,6 @@ let is_trivial = function
   | ULe (u, v) | UEq (u, v) -> Universe.equal u v
   | ULub (u, v) | UWeak (u, v) -> Level.equal u v
 
-let subst_univs fn = function
-  | ULe (u, v) ->
-    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
-    if Universe.equal u' v' then None
-    else Some (ULe (u',v'))
-  | UEq (u, v) ->
-    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
-    if Universe.equal u' v' then None
-    else Some (ULe (u',v'))
-  | ULub (u, v) ->
-    let u' = level_subst_of fn u and v' = level_subst_of fn v in
-    if Level.equal u' v' then None
-    else Some (ULub (u',v'))
-  | UWeak (u, v) ->
-    let u' = level_subst_of fn u and v' = level_subst_of fn v in
-    if Level.equal u' v' then None
-    else Some (UWeak (u',v'))
-
 module Set = struct
   module S = Set.Make(
   struct
@@ -88,11 +69,6 @@ module Set = struct
 
   let equal x y =
     x == y || equal x y
-
-  let subst_univs subst csts =
-    fold
-      (fun c -> Option.fold_right add (subst_univs subst c))
-      csts empty
 end
 
 type 'a accumulator = Set.t -> 'a -> 'a option
diff --git a/engine/univProblem.mli b/engine/univProblem.mli
index 575f5ac847..6c7a11f529 100644
--- a/engine/univProblem.mli
+++ b/engine/univProblem.mli
@@ -32,8 +32,6 @@ module Set : sig
   include Set.S with type elt = t
 
   val pr : t -> Pp.t
-
-  val subst_univs : universe_subst_fn -> t -> t
 end
 
 type 'a accumulator = Set.t -> 'a -> 'a option
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 330ed5d0ad..c76a4cd751 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -83,12 +83,6 @@ let subst_univs_constr subst c =
     let f = Univ.make_subst subst in
       subst_univs_fn_constr f c
 
-let subst_univs_constr =
-  if Flags.profile then
-    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
-      CProfile.profile2 subst_univs_constr_key subst_univs_constr
-  else subst_univs_constr
-
 let normalize_univ_variable ~find =
   let rec aux cur =
     let b = find cur in