From b0068a68675fb75dd83a384cc9739729d8dc2b9f Mon Sep 17 00:00:00 2001
From: Andrew Appel <appel@princeton.edu>
Date: Tue, 19 Mar 2024 16:31:42 -0400
Subject: [PATCH] Adapt to Coq 8.19 and CompCert 3.13.1

---
 .github/workflows/coq-action.yml | 14 +++++++-------
 Makefile                         |  2 +-
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index 4444aba9c..d8abe027f 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -21,9 +21,9 @@ jobs:
         # except for the "make_target" field and make_target related excludes
         coq_version:
           # See https://github.com/coq-community/docker-coq/wiki for supported images
-          - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
           - 'dev'
         bit_size:
           - 32
@@ -31,10 +31,10 @@ jobs:
         make_target:
           - vst
         exclude:   
-          - coq_version: 8.16
-            bit_size: 32
           - coq_version: 8.17
             bit_size: 32
+          - coq_version: 8.18
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
     steps:
@@ -53,7 +53,7 @@ jobs:
             endGroup
           install: |
             startGroup "Install dependencies"
-              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13' || 'coq-compcert.3.13' }}
+              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13.1' || 'coq-compcert.3.13.1' }}
               # Required by test2
               opam install -y coq-ext-lib
             endGroup
@@ -89,9 +89,9 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-          - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
           - 'dev' 
         make_target:
           - assumptions.txt
@@ -104,10 +104,10 @@ jobs:
           - 32
           - 64
         exclude:
-          - coq_version: 8.16
-            bit_size: 32
           - coq_version: 8.17
             bit_size: 32
+          - coq_version: 8.18
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
           - bit_size: 64
diff --git a/Makefile b/Makefile
index 84412fa86..f290f9ee1 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.16.0 or-else 8.16.1 or-else 8.17+rc1 or-else 8.17 or-else 8.17.0 or-else 8.17.1 or-else 8.18.0
+COQVERSION= 8.17.0 or-else 8.17.1 or-else 8.18.0 or-else 8.19.1
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)