diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml
index 46102bfe5..6ce4f0087 100644
--- a/.github/workflows/rocq.yml
+++ b/.github/workflows/rocq.yml
@@ -41,35 +41,35 @@ jobs:
       uses: actions/cache/restore@v5
       with:
         path: ~/.opam
-        key: ${{ matrix.version }}-with-coq-${{ hashFiles('cn.opam') }}
+        key: ${{ matrix.version }}-with-rocq-${{ hashFiles('cn.opam') }}
   
     - name: Setup OPAM
       if: steps.cache-opam-restore.outputs.cache-hit != 'true'
       run: |
         opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
-        opam switch create ${{ matrix.version }}-with-coq ${{ matrix.version }}
-        eval $(opam env --switch=${{ matrix.version }}-with-coq)
-        opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
+        opam switch create ${{ matrix.version }}-with-rocq ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }}-with-rocq)
+        opam repo add --yes --this-switch rocq-released https://coq.inria.fr/opam/released
         opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git
-        opam install --deps-only --yes ./cn.opam
+        opam install --deps-only --yes ./cn.opam ./cn-coq.opam
       
     - name: Save OPAM cache
       uses: actions/cache/save@v5
       if: steps.cache-opam-restore.outputs.cache-hit != 'true'
       with:
         path: ~/.opam
-        key: ${{ matrix.version }}-with-coq-${{ hashFiles('cn.opam') }}
+        key: ${{ matrix.version }}-with-rocq-${{ hashFiles('cn.opam') }}
 
-    - name: Install CN (with Coq)
+    - name: Install CN (with rocq)
       run: |
-        opam switch ${{ matrix.version }}-with-coq
-        eval $(opam env --switch=${{ matrix.version }}-with-coq )
+        opam switch ${{ matrix.version }}-with-rocq
+        eval $(opam env --switch=${{ matrix.version }}-with-rocq )
         opam pin --yes --no-action add cn .
         opam pin --yes --no-action add cn-coq .
         opam install --yes cn cn-coq
 
-    - name: Run CN-Coq tests
+    - name: Run CN-rocq tests
       run: |
-        opam switch ${{ matrix.version }}-with-coq
-        eval $(opam env --switch=${{ matrix.version }}-with-coq )
+        opam switch ${{ matrix.version }}-with-rocq
+        eval $(opam env --switch=${{ matrix.version }}-with-rocq )
         ./tests/diff-prog.py tests/run-cn-coq.sh tests/cn/coq.json --max-workers=2 2> diff.patch || (cat diff.patch; exit 1)
diff --git a/cn-coq.opam b/cn-coq.opam
index 9e414dafa..02e65861c 100644
--- a/cn-coq.opam
+++ b/cn-coq.opam
@@ -18,6 +18,7 @@ depends: [
   "coq" {= "8.20.1"}
   "coq-ext-lib"
   "coq-struct-tact"
+  "dune" {= "3.21.1"}
 ]
 build: [
   ["dune" "subst"] {pinned}
diff --git a/coq/Cerberus/dune b/coq/Cerberus/dune
index da7c180a4..699f6b15a 100644
--- a/coq/Cerberus/dune
+++ b/coq/Cerberus/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name Cerberus)
  (package cn-coq)
  (synopsis "Coq formalization of some Cerberus types")
diff --git a/coq/Cn/dune b/coq/Cn/dune
index 94123c240..af7310094 100644
--- a/coq/Cn/dune
+++ b/coq/Cn/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name Cn)
  (package cn-coq)
  (synopsis "Coq formalization of CN")
diff --git a/coq/Reasoning/dune b/coq/Reasoning/dune
index a1468eb50..66b7b08df 100644
--- a/coq/Reasoning/dune
+++ b/coq/Reasoning/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name Reasoning)
  (package cn-coq)
  (synopsis "CN Reasoning in Coq")
diff --git a/dune-project b/dune-project
index 273e6abb6..4e19a19f6 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.8)
+(lang dune 3.21)
 (name cn)
 
-(using coq 0.8)
+(using rocq 0.11)