diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix
index a7d8b805f067..17aaf9d55636 100644
--- a/pkgs/development/coq-modules/VST/default.nix
+++ b/pkgs/development/coq-modules/VST/default.nix
@@ -34,32 +34,17 @@ mkCoqDerivation {
   repo = "VST";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
     lib.switch coq.coq-version [
-      {
-        case = range "8.19" "8.20";
-        out = "2.15";
-      }
-      {
-        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";
-      }
+      (case (range "8.19" "8.20") "2.15")
+      (case (range "8.15" "8.19") "2.14")
+      (case (range "8.15" "8.17") "2.13")
+      (case (range "8.14" "8.16") "2.10")
+      (case (range "8.13" "8.15") "2.9")
+      (case (range "8.12" "8.13") "2.8")
     ] null;
   release."2.15".sha256 = "sha256-51k2W4efMaEO4nZ0rdkRT9rA8ZJLpot1YpFmd6RIAXw=";
   release."2.14".sha256 = "sha256-NHc1ZQ2VmXZy4lK2+mtyeNz1Qr9Nhj2QLxkPhhQB7Iw=";
@@ -73,19 +58,28 @@ mkCoqDerivation {
   buildInputs = [ ITree ];
   propagatedBuildInputs = [ compcert ];
 
-  preConfigure = ''
-    patchShebangs util
-    substituteInPlace Makefile \
-      --replace 'COQVERSION= ' 'COQVERSION= 8.20.1 or-else 8.19.2 or-else 8.17.1 or-else 8.16.1 or-else 8.16.0 or-else 8.15.2 or-else 8.15.1 or-else '\
-      --replace 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}'
-  '';
+  preConfigure =
+    ''
+      patchShebangs util
+    ''
+    +
+      lib.optionalString
+        (coq.coq-version != null && coq.coq-version != "dev" && lib.versions.isLe "8.20" coq.coq-version)
+        ''
+          substituteInPlace Makefile \
+            --replace-fail 'COQVERSION= ' 'COQVERSION= 8.20.1 or-else 8.19.2 or-else 8.17.1 or-else 8.16.1 or-else 8.16.0 or-else 8.15.2 or-else 8.15.1 or-else '\
+            --replace-fail 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}'
+        '';
 
-  makeFlags = [
-    "BITSIZE=64"
-    "COMPCERT=inst_dir"
-    "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert"
-    "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST"
-  ];
+  makeFlags =
+    [
+      "BITSIZE=64"
+      "COMPCERT=inst_dir"
+      "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert"
+      "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST"
+    ]
+    ++ lib.optional (coq.coq-version == "dev") "IGNORECOQVERSION=true"
+    ++ lib.optional (coq.coq-version == "dev") "IGNORECOMPCERTVERSION=true";
 
   postInstall = ''
     for d in msl veric floyd sepcomp progs64