diff --git a/.github/workflows/workflow.yml b/.github/workflows/workflow.yml
index f407bd4fa5f..94192298c3e 100644
--- a/.github/workflows/workflow.yml
+++ b/.github/workflows/workflow.yml
@@ -270,6 +270,26 @@ jobs:
           # We disable the Dune cache when running the tests
           DUNE_CACHE: disabled
 
+  rocq:
+    name: Rocq 9.1.0
+    needs: nix-build
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: nixbuild/nix-quick-install-action@v34
+        with:
+          nix_conf: ${{ env.EXTRA_NIX_CONFIG }}
+      - uses: nix-community/cache-nix-action@v6
+        with:
+          primary-key: |
+            nix-${{ runner.os }}-${{ github.job }}-${{ hashFiles('**/*.nix', '**/flake.lock') }}
+          restore-prefixes-first-match: nix-${{ runner.os }}-${{ github.job }}-
+          gc-max-store-size-linux: 5G
+      - run: nix develop .#rocq -c make test-coq
+        env:
+          # We disable the Dune cache when running the tests
+          DUNE_CACHE: disabled
+
   wasm:
     name: Wasm_of_ocaml
     needs: nix-build
diff --git a/flake.nix b/flake.nix
index bd035e521a1..404697c7e41 100644
--- a/flake.nix
+++ b/flake.nix
@@ -55,6 +55,14 @@
               ];
             });
           })
+          (self: super: {
+            coq_9_1_native = super.coq_9_1.overrideAttrs (a: {
+              configureFlags = [
+                "-native-compiler"
+                "yes"
+              ];
+            });
+          })
         ];
 
         applyOxcamlPatches = import ./nix/ox-patches.nix {
@@ -353,6 +361,28 @@
               '';
             };
 
+            rocq = pkgs.mkShell {
+              inherit INSIDE_NIX;
+              nativeBuildInputs = (testNativeBuildInputs pkgs);
+              # Coq requires OCaml 4.x
+              inputsFrom = [
+                pkgs.ocaml-ng.ocamlPackages_4_14.dune_3
+              ];
+              buildInputs = with pkgs; [
+                ocaml-ng.ocamlPackages_4_14.csexp
+                ocaml-ng.ocamlPackages_4_14.pp
+                ocaml-ng.ocamlPackages_4_14.re
+                ocaml-ng.ocamlPackages_4_14.spawn
+                ocaml-ng.ocamlPackages_4_14.uutf
+                coq_9_1_native
+                coq_9_1_native.ocamlPackages.findlib
+              ];
+              meta.description = ''
+                Provides a minimal shell environment built purely from nixpkgs
+                that can build Dune and the Rocq testsuite.
+              '';
+            };
+
             bootstrap-check = pkgs.mkShell {
               inherit INSIDE_NIX;
               buildInputs = with pkgs; [
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t
index 54bd7770062..a312d5cb0df 100644
--- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t
@@ -12,27 +12,27 @@ The flags passed to coqc:
   -native-compiler on
   -nI lib/coq-core/kernel
   -nI .
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . minimal
   Test.v
@@ -49,26 +49,26 @@ The flags passed to coqtop:
   -native-compiler on
   -nI lib/coq-core/kernel
   -nI $TESTCASE_ROOT/_build/default
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default minimal
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t
index 583ac167b14..490a0a7253d 100644
--- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-nested.t/run.t
@@ -19,27 +19,27 @@ Checking that we compute the directory and file for dune coq top correctly
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default/theories foo
 
@@ -52,27 +52,27 @@ Checking that we compute the directory and file for dune coq top correctly
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default/theories foo
 
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-build.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-build.t
index 74dd0e5884f..4484595c598 100644
--- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-build.t
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-no-build.t
@@ -26,27 +26,27 @@ On a fresh build, this should do nothing but should pass the correct flags:
   -nI lib/coq-core/kernel
   -nI $TESTCASE_ROOT/_build/default/dir
   -boot
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default/dir basic
 
@@ -61,26 +61,26 @@ And for comparison normally a build would happen:
   -nI lib/coq-core/kernel
   -nI $TESTCASE_ROOT/_build/default/dir
   -boot
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default/dir basic
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t
index 9907c308512..60464d9267a 100644
--- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t
@@ -29,27 +29,27 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default/dir basic
   $ dune coq top --display short --toplevel echo dir/bar.v | ../scrub_coq_args.sh
@@ -61,27 +61,27 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default/dir basic
   $ dune clean
@@ -98,27 +98,27 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default/dir basic
   $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v) | ../scrub_coq_args.sh
@@ -132,27 +132,27 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default/dir basic
 
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t
index a28e486f17e..7344db740d2 100644
--- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t
@@ -9,27 +9,27 @@ All dune commands work when you run them in sub-directories, so this should be n
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R $TESTCASE_ROOT/_build/default/theories foo
   $ cd theories
diff --git a/test/blackbox-tests/test-cases/coq/flags.t b/test/blackbox-tests/test-cases/coq/flags.t
index 02714685249..71b831ad576 100644
--- a/test/blackbox-tests/test-cases/coq/flags.t
+++ b/test/blackbox-tests/test-cases/coq/flags.t
@@ -25,27 +25,27 @@ Test case: default flags
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . foo
   foo.v
@@ -68,27 +68,27 @@ TC: :standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . foo
   foo.v
@@ -110,27 +110,27 @@ TC: override :standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . foo
   foo.v
@@ -152,27 +152,27 @@ TC: add to :standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . foo
   foo.v
@@ -199,27 +199,27 @@ TC: extend in workspace + override standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . foo
   foo.v
@@ -240,27 +240,27 @@ TC: extend in workspace + override standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . foo
   foo.v
@@ -283,27 +283,27 @@ TC: extend in dune (env) + override standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . foo
   foo.v
@@ -326,27 +326,27 @@ TC: extend in dune (env) + standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . foo
   foo.v
@@ -374,27 +374,27 @@ TC: extend in dune (env) + workspace + standard
   -w -deprecated-native-compiler-option
   -w -native-compiler-disabled
   -native-compiler ondemand
-  -I lib/coq/../coq-core/plugins/btauto
-  -I lib/coq/../coq-core/plugins/cc
-  -I lib/coq/../coq-core/plugins/derive
-  -I lib/coq/../coq-core/plugins/extraction
-  -I lib/coq/../coq-core/plugins/firstorder
-  -I lib/coq/../coq-core/plugins/funind
-  -I lib/coq/../coq-core/plugins/ltac
-  -I lib/coq/../coq-core/plugins/ltac2
-  -I lib/coq/../coq-core/plugins/micromega
-  -I lib/coq/../coq-core/plugins/nsatz
-  -I lib/coq/../coq-core/plugins/number_string_notation
-  -I lib/coq/../coq-core/plugins/ring
-  -I lib/coq/../coq-core/plugins/rtauto
-  -I lib/coq/../coq-core/plugins/ssreflect
-  -I lib/coq/../coq-core/plugins/ssrmatching
-  -I lib/coq/../coq-core/plugins/tauto
-  -I lib/coq/../coq-core/plugins/tutorial/p0
-  -I lib/coq/../coq-core/plugins/tutorial/p1
-  -I lib/coq/../coq-core/plugins/tutorial/p2
-  -I lib/coq/../coq-core/plugins/tutorial/p3
-  -I lib/coq/../coq-core/plugins/zify
+  -I .../plugins/btauto
+  -I .../plugins/cc
+  -I .../plugins/derive
+  -I .../plugins/extraction
+  -I .../plugins/firstorder
+  -I .../plugins/funind
+  -I .../plugins/ltac
+  -I .../plugins/ltac2
+  -I .../plugins/micromega
+  -I .../plugins/nsatz
+  -I .../plugins/number_string_notation
+  -I .../plugins/ring
+  -I .../plugins/rtauto
+  -I .../plugins/ssreflect
+  -I .../plugins/ssrmatching
+  -I .../plugins/tauto
+  -I .../plugins/tutorial/p0
+  -I .../plugins/tutorial/p1
+  -I .../plugins/tutorial/p2
+  -I .../plugins/tutorial/p3
+  -I .../plugins/zify
   -R coq/theories Coq
   -R . foo
   foo.v
diff --git a/test/blackbox-tests/test-cases/coq/scrub_coq_args.sh b/test/blackbox-tests/test-cases/coq/scrub_coq_args.sh
index 931e3da6324..f56a535a82e 100755
--- a/test/blackbox-tests/test-cases/coq/scrub_coq_args.sh
+++ b/test/blackbox-tests/test-cases/coq/scrub_coq_args.sh
@@ -19,9 +19,13 @@ sed 's/ -boot/\f-boot/g' | # new line for each -boot
 sed 's/ -native-compiler /\f-native-compiler /g' | # new line for each -native-compiler
 sed 's/-R [^[:space:]]*coq /-R coq /g' | # scrub -R with coq
 sed 's#-R [^[:space:]]*coq/theories #-R coq/theories #g' | # scrub -R with coq/theories
-sed 's/-I [-A-Za-z0-9\/_\.]*lib\//-I lib\//g' | # scrub -I with lib/
-sed 's/-nI [-A-Za-z0-9\/_\.]*lib\//-nI lib\//g' | # scrub -nI with lib/
+sed 's/-I [-A-Za-z0-9\/_\.+]*lib\//-I lib\//g' | # scrub -I with lib/
+sed 's/-nI [-A-Za-z0-9\/_\.+]*lib\//-nI lib\//g' | # scrub -nI with lib/
 sed 's/\(-R [^\f]* [^\f]*\) \(.*\)/\1\f\2/g' | # new line after each -R
 sed 's/\(-I lib\/findlib\)\f\(.*\)/\2\f\1/g' | # move lib/findlib to the end
 sed 's/\(-I lib\/zarith\)\f\(.*\)/\2\f\1/g' | # move lib/zarith to the end
+sed 's/lib\/coq\/[^[:space:]]*\/plugins\//...\/plugins\//g' | # normalize plugins -I
+sed 's/\f-I \.\.\.\/plugins\/[a-z]*_core\>//g' | # remove rocq-9-only plugin -I
+sed 's/\f-I \.\.\.\/plugins\/ltac2_ltac1\>//g' | # remove rocq-9-only plugin -I
+sed 's/\f-I \.\.\.\/plugins\/tutorial\/p4\>//g' | # remove rocq-9-only plugin -I
 tr '\f' '\n' # replace form feed with new line
diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/run.t b/test/blackbox-tests/test-cases/coq/vos-build.t/run.t
index 364af875235..03405e79662 100644
--- a/test/blackbox-tests/test-cases/coq/vos-build.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/vos-build.t/run.t
@@ -8,9 +8,9 @@
           coqc foo.vos
           coqc bar.vos
 
-  $ cat foo.v | dune coq top -- foo.v 2>/dev/null | sed '/^Welcome to Coq/d'
+  $ cat foo.v | dune coq top -- foo.v 2>/dev/null | sed '/^Welcome/d'
   mynat is defined
-  $ cat bar.v | dune coq top -- bar.v 2>/dev/null | sed '/^Welcome to Coq/d'
+  $ cat bar.v | dune coq top -- bar.v 2>/dev/null | sed '/^Welcome/d'
   mynum is defined
 
   $ dune clean