diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index 693559308..0e8688bfa 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -88,6 +88,8 @@ let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug =
     | Init_effect.Success w -> w)
 
 let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
+  Memprof_limits.start_memprof_limits ();
+
   (* 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/controller/lsp_core.ml b/controller/lsp_core.ml
index b8d0fe0c9..5f3f7f258 100644
--- a/controller/lsp_core.ml
+++ b/controller/lsp_core.ml
@@ -367,7 +367,7 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
     LIO.logMessage ~lvl:3 ~message;
     let result, dirs = Rq_init.do_initialize ~params in
     (* We don't need to interrupt this *)
-    let token = Coq.Limits.Token.make () in
+    let token = Coq.Limits.Token.create () in
     Rq.Action.now (Ok result) |> Rq.serve ~ofn ~token ~id;
     LIO.logMessage ~lvl:3 ~message:"Server initialized";
     (* Workspace initialization *)
@@ -463,7 +463,7 @@ let dispatch_message ~ofn ~token ~state (com : LSP.Message.t) : State.t =
 let current_token = ref None
 
 let token_factory () =
-  let token = Coq.Limits.Token.make () in
+  let token = Coq.Limits.Token.create () in
   current_token := Some token;
   token
 
diff --git a/coq/dune b/coq/dune
index ca9999b39..1c073699f 100644
--- a/coq/dune
+++ b/coq/dune
@@ -3,4 +3,4 @@
  (public_name coq-lsp.coq)
  ; Unfortunate we have to link the STM due to the LTAC plugin
  ; depending on it, we should fix this upstream
- (libraries lang coq-core.vernac coq-core.stm coq-serapi.serlib))
+ (libraries memprof-limits lang coq-core.vernac coq-core.stm coq-serapi.serlib))
diff --git a/coq/limits.ml b/coq/limits.ml
index b10590485..96a599d81 100644
--- a/coq/limits.ml
+++ b/coq/limits.ml
@@ -1,15 +1,22 @@
 (* We'd like to move this code to Lang, but it is still too specific *)
 
+module Token = Memprof_limits.Token
+
+let limit ~token ~f x =
+  let f () = f x in
+  Memprof_limits.limit_with_token ~token f
+
+module Flag = struct
 module Token : sig
   type t
 
-  val make : unit -> t
+  val create : unit -> t
   val set : t -> unit
   val is_set : t -> bool
 end = struct
   type t = bool ref
 
-  let make () = ref false
+  let create () = ref false
   let set t =
     t := true;
     Control.interrupt := true
@@ -25,3 +32,4 @@ let limit ~token ~f x =
       Ok (f x)
     with Sys.Break ->
       Error Sys.Break
+end
diff --git a/vendor/coq b/vendor/coq
index 3d227825a..42b0d3500 160000
--- a/vendor/coq
+++ b/vendor/coq
@@ -1 +1 @@
-Subproject commit 3d227825aed7d6e6ed76f8ff6483ced18c7e13ef
+Subproject commit 42b0d3500b03bdaf676b5194350a9f169e175b6f