diff --git a/pkgs/development/coq-modules/parseque/default.nix b/pkgs/development/coq-modules/parseque/default.nix
index def3689a3911..386a248f91dc 100644
--- a/pkgs/development/coq-modules/parseque/default.nix
+++ b/pkgs/development/coq-modules/parseque/default.nix
@@ -1,13 +1,14 @@
 {
   lib,
   mkCoqDerivation,
+  rocqPackages,
   which,
   coq,
   version ? null,
 }:
 
 with lib;
-mkCoqDerivation {
+(mkCoqDerivation {
   pname = "parseque";
   repo = "parseque";
   owner = "rocq-community";
@@ -19,7 +20,7 @@ mkCoqDerivation {
       [ coq.coq-version ]
       [
         {
-          cases = [ (range "8.16" "8.20") ];
+          cases = [ (range "8.16" "9.0") ];
           out = "0.2.2";
         }
       ]
@@ -30,8 +31,26 @@ mkCoqDerivation {
   releaseRev = v: "v${v}";
 
   meta = {
-    description = "Total parser combinators in Rocq";
+    description = "Total parser combinators in Coq/Rocq";
     maintainers = with maintainers; [ womeier ];
     license = licenses.mit;
   };
-}
+}).overrideAttrs
+  (
+    o:
+    # this is just a wrapper for rocPackages.parseque for Rocq >= 9.0
+    lib.optionalAttrs
+      (coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version))
+      {
+        configurePhase = ''
+          echo no configuration
+        '';
+        buildPhase = ''
+          echo building nothing
+        '';
+        installPhase = ''
+          echo installing nothing
+        '';
+        propagatedBuildInputs = [ rocqPackages.parseque ];
+      }
+  )
diff --git a/pkgs/development/rocq-modules/parseque/default.nix b/pkgs/development/rocq-modules/parseque/default.nix
new file mode 100644
index 000000000000..415ba2bc4d06
--- /dev/null
+++ b/pkgs/development/rocq-modules/parseque/default.nix
@@ -0,0 +1,40 @@
+{
+  lib,
+  mkRocqDerivation,
+  which,
+  stdlib,
+  rocq-core,
+  version ? null,
+}:
+
+with lib;
+mkRocqDerivation {
+  pname = "parseque";
+  repo = "parseque";
+  owner = "rocq-community";
+
+  inherit version;
+  defaultVersion =
+    with versions;
+    switch
+      [ rocq-core.rocq-version ]
+      [
+        {
+          cases = [ (range "9.0" "9.0") ];
+          out = "0.3.0";
+        }
+      ]
+      null;
+
+  release."0.3.0".sha256 = "sha256-W2eenv5Q421eVn2ubbninFmmdT875f3w/Zs7yGHUKP4=";
+
+  propagatedBuildInputs = [ stdlib ];
+
+  releaseRev = v: "v${v}";
+
+  meta = {
+    description = "Total parser combinators in Rocq";
+    maintainers = with maintainers; [ womeier ];
+    license = licenses.mit;
+  };
+}
diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix
index 25da5b7ac389..69a10c64bcd8 100644
--- a/pkgs/top-level/rocq-packages.nix
+++ b/pkgs/top-level/rocq-packages.nix
@@ -38,6 +38,7 @@ let
 
       bignums = callPackage ../development/rocq-modules/bignums { };
       hierarchy-builder = callPackage ../development/rocq-modules/hierarchy-builder { };
+      parseque = callPackage ../development/rocq-modules/parseque { };
       rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };
       stdlib = callPackage ../development/rocq-modules/stdlib { };