3 files changed, 25 insertions, 6 deletions
diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix
index 178db27c6379..706d11786354 100644
--- a/pkgs/development/coq-modules/VST/default.nix
+++ b/pkgs/development/coq-modules/VST/default.nix
@@ -23,11 +23,13 @@ mkCoqDerivation {
   repo = "VST";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = range "8.15" "8.19"; out = "2.14"; }
     { case = range "8.15" "8.17"; out = "2.13"; }
     { case = range "8.14" "8.16"; out = "2.10"; }
     { case = range "8.13" "8.15"; out = "2.9"; }
     { case = range "8.12" "8.13"; out = "2.8"; }
   ] null;
+  release."2.14".sha256 = "sha256-NHc1ZQ2VmXZy4lK2+mtyeNz1Qr9Nhj2QLxkPhhQB7Iw=";
   release."2.13".sha256 = "sha256-i6rvP3cpayBln5KHZOpeNfraYU5h0O9uciBQ4jRH4XA=";
   release."2.12".sha256 = "sha256-4HL0U4HA5/usKNXC0Dis1UZY/Hb/LRd2IGOrqrvdWkw=";
   release."2.11.1".sha256 = "sha256-unpNstZBnRT4dIqAYOv9n1J0tWJMeRuaaa2RG1U0Xs0=";
diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix
index 68a839cc4e8b..769017d4e282 100644
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@@ -29,7 +29,7 @@ compcert = mkCoqDerivation {
   releaseRev = v: "v${v}";
 
   defaultVersion =  with lib.versions; lib.switch coq.version [
-      { case = range "8.14" "8.17"; out = "3.13.1"; }
+      { case = range "8.14" "8.19"; out = "3.13.1"; }
       { case = isEq "8.13"        ; out = "3.10"; }
       { case = isEq "8.12"       ; out = "3.9"; }
       { case = range "8.8" "8.11"; out = "3.8"; }
@@ -170,12 +170,27 @@ compcert.overrideAttrs (o:
           })
         ];
       }
-      { cases = [ (isEq "8.17") (isEq "3.13") ];
+      { cases = [ (range "8.17" "8.19") (isEq "3.13") ];
         out = [
           # Support for Coq 8.17.0 & Coq 8.17.1
           (fetchpatch {
-            url = "https://github.com/AbsInt/CompCert/commit/030a0fafe6a1a315bb13c5276e0af536e4f713ce.patch";
-            hash = "sha256-iRdmgYuun1wp6chRoDy99KKmFyvY79NGWzrltyQaW1o=";
+            url = "https://github.com/AbsInt/CompCert/commit/2e04d986bdae578186e40330842878559a550402.patch";
+            hash = "sha256-2ZRAjUUSScJI8ogWFTnukCUnJdLWGvyOPyfIVlHL4ig=";
+          })
+          # Support for Coq 8.18.0
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/28218c5663cba36c6078ca342335d4e55c412bd7.patch";
+            hash = "sha256-aAatUMO26oZwFYGh1BXYWxbTuyOgU8BAKMGDS5796hM=";
+          })
+          # MenhirLib update
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/9f3d7b6eb99377ad4689cd57563c484c57baa457.patch";
+            hash = "sha256-paofdSBxP/JFoBSiO1OI+mjKRI3UCanXRh/drzYt93E=";
+          })
+          # Support for Coq 8.19.0 & Coq 8.19.1
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/a2e4ed62fc558d565366845f9d135bd7db5e23c4.patch";
+            hash = "sha256-ufk0bokuayLfkSvK3cK4E9iXU5eZpp9d/ETSa/zCfMg=";
           })
         ];
       }
diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix
index 52d4799eb173..0183de981226 100644
--- a/pkgs/development/coq-modules/mathcomp-word/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-word/default.nix
@@ -18,15 +18,17 @@ mkCoqDerivation {
 
   releaseRev = v: "v${v}";
 
+  release."3.1".sha256 = "sha256-qQHis6554sG7NpCpWhT2wvelnxsrbEPVNv3fpxwxHMU=";
   release."3.0".sha256 = "sha256-xEgx5HHDOimOJbNMtIVf/KG3XBemOS9XwoCoW6btyJ4=";
+  release."2.3".sha256 = "sha256-whU1yvFFuxpwQutW41B/WBg5DrVZJW/Do/GuHtzuI3U=";
   release."2.2".sha256 = "sha256-8BB6SToCrMZTtU78t2K+aExuxk9O1lCqVQaa8wabSm8=";
   release."2.1".sha256 = "sha256-895gZzwwX8hN9UUQRhcgRlphHANka9R0PRotfmSEelA=";
   release."2.0".sha256 = "sha256-ySg3AviGGY5jXqqn1cP6lTw3aS5DhawXEwNUgj7pIjA=";
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
-    { cases = [ (range "8.16" "8.19") (isGe "2.0")          ]; out = "3.0"; }
-    { cases = [ (range "8.12" "8.19") (range "1.12" "1.19") ]; out = "2.2"; }
+    { cases = [ (range "8.16" "8.19") (isGe "2.0")          ]; out = "3.1"; }
+    { cases = [ (range "8.12" "8.19") (range "1.12" "1.19") ]; out = "2.3"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];