From 82dc1d72251cca2e45e654fc1cfe62aee9b69538 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 11 Feb 2025 14:54:17 +0100
Subject: [PATCH] coqPackages.VST: 2.14 -> 2.15

---
 pkgs/development/coq-modules/VST/default.nix | 7 ++++++-
 pkgs/top-level/coq-packages.nix              | 2 +-
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix
index d82699847d01f..a7d8b805f0675 100644
--- a/pkgs/development/coq-modules/VST/default.nix
+++ b/pkgs/development/coq-modules/VST/default.nix
@@ -36,6 +36,10 @@ mkCoqDerivation {
   defaultVersion =
     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";
@@ -57,6 +61,7 @@ mkCoqDerivation {
         out = "2.8";
       }
     ] null;
+  release."2.15".sha256 = "sha256-51k2W4efMaEO4nZ0rdkRT9rA8ZJLpot1YpFmd6RIAXw=";
   release."2.14".sha256 = "sha256-NHc1ZQ2VmXZy4lK2+mtyeNz1Qr9Nhj2QLxkPhhQB7Iw=";
   release."2.13".sha256 = "sha256-i6rvP3cpayBln5KHZOpeNfraYU5h0O9uciBQ4jRH4XA=";
   release."2.12".sha256 = "sha256-4HL0U4HA5/usKNXC0Dis1UZY/Hb/LRd2IGOrqrvdWkw=";
@@ -71,7 +76,7 @@ mkCoqDerivation {
   preConfigure = ''
     patchShebangs util
     substituteInPlace Makefile \
-      --replace 'COQVERSION= ' 'COQVERSION= 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 '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}'
   '';
 
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 1974d65304fa0..372c95eb3df40 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -171,7 +171,7 @@ let
         (lib.versionAtLeast self.coq.version "8.14") {
           compcert = self.compcert.override {
             version = with lib.versions; lib.switch self.coq.version [
-              { case = range "8.15" "8.19"; out = "3.13.1"; }
+              { case = range "8.15" "8.18"; out = "3.13.1"; }
               { case = isEq "8.14"; out = "3.11"; }
             ] null;
           };