diff --git a/compiler/cc.ml b/compiler/cc.ml
index 828e2bd4b..c81bf7738 100644
--- a/compiler/cc.ml
+++ b/compiler/cc.ml
@@ -4,4 +4,5 @@ type t =
   ; workspaces : (string * (Coq.Workspace.t, string) Result.t) list
   ; default : Coq.Workspace.t
   ; io : Fleche.Io.CallBack.t
+  ; token : Coq.Limits.Token.t
   }
diff --git a/compiler/compile.ml b/compiler/compile.ml
index e9282f6f3..50bfbc071 100644
--- a/compiler/compile.ml
+++ b/compiler/compile.ml
@@ -25,7 +25,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
   Util.format_to_file ~file ~f:Output.pp_diags diags
 
 let compile_file ~cc file =
-  let { Cc.io; root_state; workspaces; default } = cc in
+  let { Cc.io; root_state; workspaces; default; token } = cc in
   let lvl = Io.Level.info in
   let message = Format.asprintf "compiling file %s@\n%!" file in
   io.message ~lvl ~message;
@@ -35,7 +35,6 @@ let compile_file ~cc file =
     let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
     let env = Doc.Env.make ~init:root_state ~workspace in
     let raw = Util.input_all file in
-    let token = Coq.Limits.Token.create () in
     let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io ~token with
     | None -> ()
diff --git a/compiler/driver.ml b/compiler/driver.ml
index 2a9cf34c5..a8062b63e 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -37,6 +37,7 @@ let go args =
   let root_state = coq_init ~debug in
   let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in
   let default = Coq.Workspace.default ~debug ~cmdline in
+  let () = Coq.Limits.start () in
   let token = Coq.Limits.Token.create () in
   let workspaces =
     List.map
@@ -44,7 +45,7 @@ let go args =
       roots
   in
   List.iter (log_workspace ~io) workspaces;
-  let cc = Cc.{ root_state; workspaces; default; io } in
+  let cc = Cc.{ root_state; workspaces; default; io; token } in
   (* Initialize plugins *)
   plugin_init plugins;
   Compile.compile ~cc files
diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index 993aaa0d4..aad1d0fba 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -95,6 +95,8 @@ let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug =
 
 let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
     require_libraries delay =
+  Coq.Limits.start ();
+
   (* Try to be sane w.r.t. \r\n in Windows *)
   Stdlib.set_binary_mode_in stdin true;
   Stdlib.set_binary_mode_out stdout true;
diff --git a/coq/limits.ml b/coq/limits.ml
index 5b52aa222..f31f8cd39 100644
--- a/coq/limits.ml
+++ b/coq/limits.ml
@@ -46,5 +46,4 @@ module Coq : Intf = struct
 end
 
 module Mp = Limits_mp_impl
-
-include Coq
+include Mp
diff --git a/coq/limits.mli b/coq/limits.mli
index cc21cf585..c342ccd73 100644
--- a/coq/limits.mli
+++ b/coq/limits.mli
@@ -16,5 +16,4 @@ end
 
 module Coq : Intf
 module Mp : Intf
-
 include Intf
diff --git a/vendor/coq b/vendor/coq
index f73a25d38..d2998cf22 160000
--- a/vendor/coq
+++ b/vendor/coq
@@ -1 +1 @@
-Subproject commit f73a25d383465d06c1e0ab64a0784b68d3a6e2e4
+Subproject commit d2998cf2290faa0e5dea4240aa92d39a24094d91