diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 4bda2900c..dbf9e6452 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -169,7 +169,7 @@ jobs:
         run: |
           opam install lwt logs # Also build pet-server
           opam install memprof-limits # We need to do this to avoid coq-lsp rebuilding Coq below due to deptops
-          opam install vendor/coq/{coq-core,coq-stdlib,coqide-server,coq}.opam
+          opam install vendor/coq/{coq-core,rocq-core,coq-stdlib,coqide-server,coq}.opam
 
       - name: Install `coq-lsp` into OPAM switch
         run: opam install .
diff --git a/Makefile b/Makefile
index 21f55c73a..ff23f773b 100644
--- a/Makefile
+++ b/Makefile
@@ -4,7 +4,8 @@ COQ_BUILD_CONTEXT=../_build/default/coq
 
 PKG_SET= \
 vendor/coq/coq-core.install \
-vendor/coq/coq-stdlib.install \
+vendor/coq/rocq-core.install \
+vendor/coq/stdlib/coq-stdlib.install \
 coq-lsp.install
 
 # Get the ocamlformat version from the .ocamlformat file
@@ -61,6 +62,7 @@ vendor/coq/config/coq_config.ml: vendor/coq
 	        -libdir "$$EPATH/_build/install/default/lib/coq" \
 	        -bytecode-compiler $(COQVM) \
 		-native-compiler no \
+	&& sed -i.bak 's/\((dirs .*\)/; \1/g' dune \
 	&& cp theories/dune.disabled theories/dune \
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
 
@@ -74,10 +76,10 @@ winconfig:
 	&& ./configure -no-ask -prefix "$$EPATH\\_build\\install\\default\\" \
 	        -libdir "$$EPATH\\_build\\install\\default\\lib\\coq\\" \
 		-native-compiler no \
+	&& sed -i.bak 's/\((dirs .*\)/; \1/g' dune \
 	&& cp theories/dune.disabled theories/dune \
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
 
-
 .PHONY: js
 js: COQVM = no
 js: coq_boot
@@ -144,7 +146,7 @@ make-fmt: build fmt
 .PHONY: opam-update-and-reinstall
 opam-update-and-reinstall:
 	git pull --recurse-submodules
-	for pkg in coq-core coq-stdlib coqide-server coq; do opam install -y vendor/coq/$$pkg.opam; done
+	for pkg in coq-core rocq-core stdlib/coq-stdlib coqide-server coq; do opam install -y vendor/coq/$$pkg.opam; done
 	opam install .
 
 .PHONY: patch-for-js
diff --git a/coq/workspace.ml b/coq/workspace.ml
index a5677182e..59c159633 100644
--- a/coq/workspace.ml
+++ b/coq/workspace.ml
@@ -86,7 +86,7 @@ let hash = Hashtbl.hash
 let compare = Stdlib.compare
 
 (* Lib setup, XXX unify with sysinit *)
-let coq_root = Names.DirPath.make [ Libnames.coq_root ]
+let coq_root = Names.DirPath.make [ Libnames.rocq_init_root ]
 let default_root = Libnames.default_root_prefix
 
 let mk_lp ~coq_path ~unix_path ~implicit =
diff --git a/vendor/coq b/vendor/coq
index 4923ec097..7870106c5 160000
--- a/vendor/coq
+++ b/vendor/coq
@@ -1 +1 @@
-Subproject commit 4923ec0974ed45a74abebf067506696a172ab5de
+Subproject commit 7870106c52979caa3e913135915a0e0b6a459f65