diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix
index 0e7225a184a..acde0cdb84c 100644
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@@ -14,7 +14,7 @@ let compcert = mkCoqDerivation rec {
   releaseRev = v: "v${v}";
 
   defaultVersion =  with lib.versions; lib.switch coq.version [
-      { case = range "8.14" "8.16"; out = "3.11"; }
+      { case = range "8.14" "8.16"; out = "3.12"; }
       { case = isEq "8.13"        ; out = "3.10"; }
       { case = isEq "8.12"       ; out = "3.9"; }
       { case = range "8.8" "8.11"; out = "3.8"; }
@@ -25,6 +25,7 @@ let compcert = mkCoqDerivation rec {
     "3.9".sha256 = "1srcz2dqrvmbvv5cl66r34zqkm0hsbryk7gd3i9xx4slahc9zvdb";
     "3.10".sha256 = "sha256:19rmx8r8v46101ij5myfrz60arqjy7q3ra3fb8mxqqi3c8c4l4j6";
     "3.11".sha256 = "sha256-ZISs/ZAJVWtxp9+Sg5qV5Rss1gI9hK769GnBfawLa6A=";
+    "3.12".sha256 = "sha256-hXkQ8UnAx3k50OJGBmSm4hgrnRFCosu4+PEMrcKfmV0=";
   };
 
   strictDeps = true;
@@ -138,7 +139,7 @@ compcert.overrideAttrs (o:
           })
         ];
       }
-      { cases = [ (isEq "8.16") "3.11" ];
+      { cases = [ (isEq "8.16") (range "3.11" "3.12") ];
         out = [
           # Support for Coq 8.16.0
           (fetchpatch {
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 64121de7ca4..0b9148d2bb6 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -112,7 +112,10 @@ let
       trakt = callPackage ../development/coq-modules/trakt {};
       Velisarios = callPackage ../development/coq-modules/Velisarios {};
       Verdi = callPackage ../development/coq-modules/Verdi {};
-      VST = callPackage ../development/coq-modules/VST {};
+      VST = callPackage ../development/coq-modules/VST (lib.optionalAttrs
+        (lib.versionAtLeast self.coq.version "8.14") {
+          compcert = self.compcert.override { version = "3.11"; };
+        });
       zorns-lemma = callPackage ../development/coq-modules/zorns-lemma {};
       filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
     };