diff --git a/.gitmodules b/.gitmodules
index 5686103..5fb5ef3 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,12 +1,14 @@
 [submodule "rocq"]
 	path = rocq
-	url = git@github.com:rocq-prover/rocq.git
+	url = git@github.com:impermeable/rocq.git
+        branch = wp_proof_mode
+[submodule "coq-waterproof"]
+	path = coq-waterproof
+	url = git@github.com:impermeable/coq-waterproof.git
+        branch = wp_proof_mode
 [submodule "stdlib"]
 	path = stdlib
 	url = git@github.com:rocq-prover/stdlib.git
 [submodule "coq-lsp"]
 	path = coq-lsp
 	url = git@github.com:ejgallego/coq-lsp.git
-[submodule "coq-waterproof"]
-	path = coq-waterproof
-	url = git@github.com:impermeable/coq-waterproof.git
diff --git a/Makefile b/Makefile
index 06b1396..5b5e7f1 100644
--- a/Makefile
+++ b/Makefile
@@ -5,7 +5,7 @@ PKG_SET=coq-lsp/coq-lsp.install rocq/coq-core.install rocq/rocq-core.install roc
 
 .PHONY: build
 build: rocq/config/coq_config.ml
-	dune build $(PKG_SET)
+	dune build $(DUNEOPT) $(PKG_SET)
 
 # Ideally we could regenerate this on Rocq updates, usually not needed
 rocq/config/coq_config.ml: rocq
@@ -37,7 +37,7 @@ clean:
 
 # Test
 .PHONY: test
-launch: build
+test: build
 	echo "Test not implemented"
 
 # Launch where the _CoqProject file is
diff --git a/README.md b/README.md
index 017fcfc..5e0c0c8 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,10 @@
 ## Waterproof Dev environment
 
-This is a meta-project providing a setup to build coq-waterproof against the Rocq master branch along with master branches of other tools.
+This is a meta-project providing a setup to build coq-waterproof
+against the Rocq master branch along with master branches of other
+tools.
 
-Building is done using `make all`.
+Building is done using `make`.
 
 To use `coq-lsp` in vscode, one can then run
 
@@ -16,3 +18,13 @@ To execute tests against the Waterproof exercises, run
 ```
 dune test
 ```
+## Branch setup for the composed build
+
+As of today, we have two specific branches for the Waterproof proof
+mode setup, in particular for Rocq and Waterproof, we store the
+changes in the `wp_proof_mode` branch at the impermeable repository:
+
+- https://github.com/impermeable/coq-waterproof/tree/wp_proof_mode
+- https://github.com/impermeable/rocq/tree/wp_proof_mode
+- stdlib: we use the main branch
+- coq-lsp: we use the main branch
diff --git a/coq-lsp b/coq-lsp
index 8812ff6..edc3998 160000
--- a/coq-lsp
+++ b/coq-lsp
@@ -1 +1 @@
-Subproject commit 8812ff6b00d5738517c5e40af94e0ad4988176ef
+Subproject commit edc3998369e93d1f9707ebbab5989e6e400b7d67
diff --git a/coq-waterproof b/coq-waterproof
index dd712eb..1bced0c 160000
--- a/coq-waterproof
+++ b/coq-waterproof
@@ -1 +1 @@
-Subproject commit dd712eb0b7f5c205870dbd156736a684d40eeb9a
+Subproject commit 1bced0c3c23bd6a1541ef23ed2edb2d262db60de
diff --git a/rocq b/rocq
index be26673..4015c7e 160000
--- a/rocq
+++ b/rocq
@@ -1 +1 @@
-Subproject commit be266736842a4ee7ef860bb7d7dc24769596a635
+Subproject commit 4015c7e4126a1aca4abef8a72bede16a54a1f0a5
diff --git a/stdlib b/stdlib
index 71a6beb..e307464 160000
--- a/stdlib
+++ b/stdlib
@@ -1 +1 @@
-Subproject commit 71a6beb0b14452fe8042d1c010b56be4b66403c0
+Subproject commit e30746402e2bc0ef6a5dd5ad2c365ef0bc78f995