diff --git a/pkgs/development/coq-modules/parseque/default.nix b/pkgs/development/coq-modules/parseque/default.nix
new file mode 100644
index 000000000000..def3689a3911
--- /dev/null
+++ b/pkgs/development/coq-modules/parseque/default.nix
@@ -0,0 +1,37 @@
+{
+  lib,
+  mkCoqDerivation,
+  which,
+  coq,
+  version ? null,
+}:
+
+with lib;
+mkCoqDerivation {
+  pname = "parseque";
+  repo = "parseque";
+  owner = "rocq-community";
+
+  inherit version;
+  defaultVersion =
+    with versions;
+    switch
+      [ coq.coq-version ]
+      [
+        {
+          cases = [ (range "8.16" "8.20") ];
+          out = "0.2.2";
+        }
+      ]
+      null;
+
+  release."0.2.2".sha256 = "sha256-O50Rs7Yf1H4wgwb7ltRxW+7IF0b04zpfs+mR83rxT+E=";
+
+  releaseRev = v: "v${v}";
+
+  meta = {
+    description = "Total parser combinators in Rocq";
+    maintainers = with maintainers; [ womeier ];
+    license = licenses.mit;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 81c9423e6b21..83cc3bde1585 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -187,6 +187,7 @@ let
       paco = callPackage ../development/coq-modules/paco { };
       paramcoq = callPackage ../development/coq-modules/paramcoq { };
       parsec = callPackage ../development/coq-modules/parsec { };
+      parseque = callPackage ../development/coq-modules/parseque { };
       pocklington = callPackage ../development/coq-modules/pocklington { };
       QuickChick = callPackage ../development/coq-modules/QuickChick { };
       reglang = callPackage ../development/coq-modules/reglang { };