diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix
index 033fc30330f2..8b3563253c55 100644
--- a/pkgs/development/coq-modules/stdlib/default.nix
+++ b/pkgs/development/coq-modules/stdlib/default.nix
@@ -16,16 +16,20 @@
   defaultVersion =
     with lib.versions;
     lib.switch coq.version [
-      { case = isEq "9.0"; out = "9.0+rc1"; }
-      { case = isLt "8.21"; out = "8.20"; }
+      { case = isEq "9.0"; out = "9.0.0"; }
+      # the one below is artificial as stdlib was included in Coq before
+      { case = isLt "9.0"; out = "9.0.0"; }
     ] null;
   releaseRev = v: "V${v}";
 
-  release."9.0+rc1".sha256 = "sha256-raHwniQdpAX1HGlMofM8zVeXcmlUs+VJZZg5VF43k/M=";
-  release."8.20".sha256 = "sha256-AcoS4edUYCfJME1wx8UbuSQRF3jmxhArcZyPIoXcfu0=";
-
-  useDune = true;
+  release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
 
+  configurePhase = ''
+    echo no configuration
+  '';
+  buildPhase = ''
+    echo building nothing
+  '';
   installPhase = ''
     echo installing nothing
   '';
@@ -40,12 +44,6 @@
     o:
     # stdlib is already included in Coq <= 8.20
     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
       '';
diff --git a/pkgs/development/rocq-modules/stdlib/default.nix b/pkgs/development/rocq-modules/stdlib/default.nix
index 6bfce6dacf24..2686c0f8ca7c 100644
--- a/pkgs/development/rocq-modules/stdlib/default.nix
+++ b/pkgs/development/rocq-modules/stdlib/default.nix
@@ -15,29 +15,15 @@ mkRocqDerivation {
   defaultVersion =
     with lib.versions;
     lib.switch rocq-core.version [
-      { case = isEq "9.0"; out = "9.0+rc1"; }
-      { case = isLt "8.21"; out = "8.20"; }
+      { case = isEq "9.0"; out = "9.0.0"; }
+      # the one below is artificial as stdlib was included in Coq before
+      { case = isLt "9.0"; out = "9.0.0"; }
     ] null;
   releaseRev = v: "V${v}";
 
-  release."9.0+rc1".sha256 = "sha256-raHwniQdpAX1HGlMofM8zVeXcmlUs+VJZZg5VF43k/M=";
-  release."8.20".sha256 = "sha256-AcoS4edUYCfJME1wx8UbuSQRF3jmxhArcZyPIoXcfu0=";
+  release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
 
-  useDune = true;
-
-  configurePhase = ''
-    patchShebangs dev/with-rocq-wrap.sh
-  '';
-
-  buildPhase = ''
-    dev/with-rocq-wrap.sh dune build -p rocq-stdlib @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
-  '';
-
-  installPhase = ''
-    dev/with-rocq-wrap.sh dune install --root . rocq-stdlib --prefix=$out --libdir $OCAMLFIND_DESTDIR
-    mkdir $out/lib/coq/
-    mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${rocq-core.rocq-version}
-  '';
+  mlPlugin = true;
 
   meta = {
     description = "The Rocq Proof Assistant -- Standard Library";