7 files changed, 17 insertions, 17 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 5d9b595d36..a356f32e9d 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -49,7 +49,7 @@ end
 
 type expiration = bool ref
 
-module Make(T : Task) = struct
+module Make(T : Task) () = struct
 
   exception Die
   type response =
@@ -107,7 +107,7 @@ module Make(T : Task) = struct
     let open Feedback in
     feedback ~id:Stateid.initial (WorkerStatus(id, s))
 
-  module Worker = Spawn.Sync(struct end)
+  module Worker = Spawn.Sync ()
 
   module Model = struct
 
@@ -354,5 +354,5 @@ module Make(T : Task) = struct
 
 end
 
-module MakeQueue(T : Task) = struct include Make(T) end
-module MakeWorker(T : Task) = struct include Make(T) end
+module MakeQueue(T : Task) () = struct include Make(T) () end
+module MakeWorker(T : Task) () = struct include Make(T) () end
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index a80918e933..1044e668b6 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -41,7 +41,7 @@ end
 
 type expiration = bool ref
 
-module MakeQueue(T : Task) : sig
+module MakeQueue(T : Task) () : sig
 
   type queue
 
@@ -76,7 +76,7 @@ module MakeQueue(T : Task) : sig
 
 end
 
-module MakeWorker(T : Task) : sig
+module MakeWorker(T : Task) () : sig
 
   val main_loop : unit -> unit
   val init_stdout : unit -> unit
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index a27c6d6cd2..10b42f7e91 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask)
+module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
 
 let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index ac7a270ac6..a1fe50c63e 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask)
+module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
 
 let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 84a4c5cc52..6c22d3771d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -179,7 +179,7 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *)
 let default_info () =
   { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
 
-module DynBlockData : Dyn.S = Dyn.Make(struct end)
+module DynBlockData : Dyn.S = Dyn.Make ()
 
 (* Clusters of nodes implemented as Dag properties.  While Dag and Vcs impose
  * no constraint on properties, here we impose boxes to be non overlapping.
@@ -517,8 +517,8 @@ end = struct (* {{{ *)
   let reachable id = reachable !vcs id
   let mk_branch_name { expr = x } = Branch.make
     (let rec aux x = match x with
-    | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
-    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i
+    | VernacDefinition (_,((_,i),_),_) -> Names.Id.to_string i
+    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.Id.to_string i
     | VernacTime (_, e)
     | VernacTimeout (_, e) -> aux e
     | _ -> "branch" in aux x)
@@ -1558,7 +1558,7 @@ and Slaves : sig
 
 end = struct (* {{{ *)
 
-  module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask)
+  module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) ()
   
   let queue = ref None
   let init () =
@@ -1884,7 +1884,7 @@ and Partac : sig
 
 end = struct (* {{{ *)
     
-  module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
+  module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
 
   let vernac_interp ~solve ~abstract cancel nworkers safe_id id
     { indentation; verbose; loc; expr = e; strlen }
@@ -2014,7 +2014,7 @@ and Query : sig
 
 end = struct (* {{{ *)
 
-  module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask)
+  module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask) ()
 
   let queue = ref None
 
@@ -3097,7 +3097,7 @@ let current_proof_depth ~doc =
 let unmangle n =
   let n = VCS.Branch.to_string n in
   let idx = String.index n '_' + 1 in
-  Names.id_of_string (String.sub n idx (String.length n - idx))
+  Names.Id.of_string (String.sub n idx (String.length n - idx))
 
 let proofname b = match VCS.get_branch b with
   | { VCS.kind = (`Proof _| `Edit _) } -> Some b
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index 1716ac0c61..17f90b7b15 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module W = AsyncTaskQueue.MakeWorker(Stm.TacTask)
+module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
 
 let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 9507e90ba7..da6a095ab7 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -14,7 +14,7 @@ let check_vio (ts,f) =
   Stm.set_compilation_hints long_f_dot_v;
   List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
 
-module Worker = Spawn.Sync(struct end)
+module Worker = Spawn.Sync ()
 
 module IntOT = struct
   type t = int