diff --git a/pkgs/development/coq-modules/MenhirLib/default.nix b/pkgs/development/coq-modules/MenhirLib/default.nix
index 5b680c73da44..c94e0f95c49a 100644
--- a/pkgs/development/coq-modules/MenhirLib/default.nix
+++ b/pkgs/development/coq-modules/MenhirLib/default.nix
@@ -14,14 +14,8 @@ let
     defaultVersion =
       with lib.versions;
       lib.switch coq.coq-version [
-        {
-          case = range "8.12" "8.20";
-          out = "20240715";
-        }
-        {
-          case = range "8.7" "8.11";
-          out = "20200624";
-        }
+        { case = range "8.12" "8.20"; out = "20240715"; }
+        { case = range "8.7" "8.11"; out = "20200624"; }
       ] null;
     release = {
       "20240715".sha256 = "sha256-9CSxAIm0aEXkwF+aj8u/bqLG30y5eDNz65EnohJPjzI="; # coq 8.9 - 8.20
diff --git a/pkgs/development/coq-modules/json/default.nix b/pkgs/development/coq-modules/json/default.nix
new file mode 100644
index 000000000000..6638c8b211db
--- /dev/null
+++ b/pkgs/development/coq-modules/json/default.nix
@@ -0,0 +1,26 @@
+{ lib, mkCoqDerivation, coq, parsec, MenhirLib, version ? null }:
+
+mkCoqDerivation {
+  pname = "json";
+  owner = "liyishuai";
+  repo = "coq-json";
+  inherit version;
+
+  defaultVersion = let inherit (lib.versions) range; in
+    lib.switch coq.coq-version [
+      { case = range "8.14" "8.20"; out = "0.1.3"; }
+    ] null;
+  release = {
+    "0.1.3".sha256  = "sha256-lElAzW4IuX+BB6ngDjlyKn0MytLRfbhQanB+Lct/WR0=";
+  };
+  releaseRev = v: "v${v}";
+
+  propagatedBuildInputs = [ parsec MenhirLib coq.ocamlPackages.menhir ];
+
+  buildFlags = [ "MENHIRFLAGS=--coq" "MENHIRFLAGS+=--coq-no-version-check" ];
+
+  meta = {
+    description = "From JSON to Coq, and vice versa.";
+    license = lib.licenses.bsd3;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index ef7c315cca46..ad50cb242455 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -80,6 +80,7 @@ let
       itauto = callPackage ../development/coq-modules/itauto { };
       ITree = callPackage ../development/coq-modules/ITree { };
       itree-io = callPackage ../development/coq-modules/itree-io { };
+      json = callPackage ../development/coq-modules/json {};
       LibHyps = callPackage ../development/coq-modules/LibHyps {};
       ltac2 = callPackage ../development/coq-modules/ltac2 {};
       math-classes = callPackage ../development/coq-modules/math-classes { };