diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 848a69a3f2cc..895d3fb2c9bf 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -13,6 +13,7 @@
 , buildIde ? null # default is true for Coq < 8.14 and false for Coq >= 8.14
 , glib, adwaita-icon-theme, wrapGAppsHook3, makeDesktopItem, copyDesktopItems
 , csdp ? null
+, rocq-core  # for versions >= 9.0 that are transition shims on top of Rocq
 , version, coq-version ? null
 }@args:
 let
@@ -207,9 +208,6 @@ self = stdenv.mkDerivation {
     cp bin/votour $out/bin/
   '' + ''
     ln -s $out/lib/coq${suffix} $OCAMLFIND_DESTDIR/coq${suffix}
-  '' + lib.optionalString (coqAtLeast "8.21") ''
-    ln -s $out/lib/rocq-runtime $OCAMLFIND_DESTDIR/rocq-runtime
-    ln -s $out/lib/rocq-core $OCAMLFIND_DESTDIR/rocq-core
   '' + lib.optionalString (coqAtLeast "8.14") ''
     ln -s $out/lib/coqide-server $OCAMLFIND_DESTDIR/coqide-server
   '' + lib.optionalString buildIde ''
@@ -233,17 +231,24 @@ self = stdenv.mkDerivation {
     mainProgram = "coqide";
   };
 }; in
-if coqAtLeast "8.21" then self.overrideAttrs(_: {
+if coqAtLeast "8.21" then self.overrideAttrs(o: {
   # coq-core is now a shim for rocq
+  propagatedBuildInputs = o.propagatedBuildInputs ++ [ rocq-core ];
   buildPhase = ''
     runHook preBuild
-    make dunestrap
-    dune build -p rocq-runtime,rocq-core,coq-core,coqide-server${lib.optionalString buildIde ",rocqide"} -j $NIX_BUILD_CORES
+    dune build -p coq-core,coqide-server${lib.optionalString buildIde ",rocqide"} -j $NIX_BUILD_CORES
     runHook postBuild
   '';
   installPhase = ''
     runHook preInstall
-    dune install --prefix $out rocq-runtime rocq-core coq-core coqide-server${lib.optionalString buildIde " rocqide"}
+    dune install --prefix $out coq-core coqide-server${lib.optionalString buildIde " rocqide"}
+    # coq and rocq are now in different directories, which sometimes confuses coq_makefile
+    # which expects both in the same /nix/store/.../bin/ directory
+    # adding symlinks to content it
+    ROCQBIN=$(dirname ''$(command -v rocq))
+    for b in csdpcert ocamllibdep rocq rocq.byte rocqchk votour ; do
+      ln -s ''${ROCQBIN}/''${b} $out/bin/
+    done
     runHook postInstall
   '';
 }) else if coqAtLeast "8.17" then self.overrideAttrs(_: {
diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix
index cac0c4b53405..033fc30330f2 100644
--- a/pkgs/development/coq-modules/stdlib/default.nix
+++ b/pkgs/development/coq-modules/stdlib/default.nix
@@ -1,5 +1,6 @@
 {
   coq,
+  rocqPackages,
   mkCoqDerivation,
   lib,
   version ? null,
@@ -25,22 +26,12 @@
 
   useDune = true;
 
-  configurePhase = ''
-    patchShebangs dev/with-rocq-wrap.sh
-  '';
-
-  buildPhase = ''
-    dev/with-rocq-wrap.sh dune build -p rocq-stdlib,coq-stdlib @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
-  '';
-
   installPhase = ''
-    dev/with-rocq-wrap.sh dune install --root . rocq-stdlib coq-stdlib --prefix=$out --libdir $OCAMLFIND_DESTDIR
-    mkdir $out/lib/coq/
-    mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
+    echo installing nothing
   '';
 
   meta = {
-    description = "Coq Standard Library";
+    description = "Compatibility metapackage for Coq Stdlib library after the Rocq renaming";
     license = lib.licenses.lgpl21Only;
   };
 
@@ -48,14 +39,15 @@
   (
     o:
     # stdlib is already included in Coq <= 8.20
-    lib.optionalAttrs
-      (coq.version != null && coq.version != "dev" && lib.versions.isLt "8.21" coq.version)
-      {
-        buildPhase = ''
-          echo building nothing
-        '';
-        installPhase = ''
-          touch $out
-        '';
-      }
+    if coq.version != null && coq.version != "dev" && lib.versions.isLt "8.21" coq.version then {
+      configurePhase = ''
+        echo no configuration
+      '';
+      buildPhase = ''
+        echo building nothing
+      '';
+      installPhase = ''
+        touch $out
+      '';
+    } else { propagatedBuildInputs = [ rocqPackages.stdlib ]; }
   )
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 8e6ac8cafe4c..1974d65304fa 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -235,7 +235,7 @@ in rec {
   coq_8_18 = mkCoq "8.18";
   coq_8_19 = mkCoq "8.19";
   coq_8_20 = mkCoq "8.20";
-  coq_9_0 = mkCoq "9.0";
+  coq_9_0  = mkCoq "9.0+rc1";
 
   coqPackages_8_5 = mkCoqPackages coq_8_5;
   coqPackages_8_6 = mkCoqPackages coq_8_6;