diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index 12155f26b..8e0729dde 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -21,9 +21,8 @@ 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.17'
-          - '8.18'
           - '8.19'
+          - '8.20'
           - 'dev'
         bit_size:
           - 32
@@ -31,9 +30,7 @@ jobs:
         make_target:
           - vst
         exclude:   
-#         - coq_version: 8.17
-#            bit_size: 32
-          - coq_version: 8.18
+          - coq_version: 8.19
             bit_size: 32
           - coq_version: dev
             bit_size: 32
@@ -91,9 +88,8 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-#          - '8.17'
-          - '8.18'
           - '8.19'
+          - '8.20'
           - 'dev' 
         make_target:
           - assumptions.txt
@@ -106,9 +102,7 @@ jobs:
           - 32
           - 64
         exclude:
-#          - coq_version: 8.17
-#            bit_size: 32
-          - coq_version: 8.18
+          - coq_version: 8.19
             bit_size: 32
           - coq_version: dev
             bit_size: 32
diff --git a/Makefile b/Makefile
index 27b8bfdbd..d3d291dac 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.17.0 or-else 8.17.1 or-else 8.18.0 or-else 8.19.1
+COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)
@@ -334,6 +334,11 @@ DEPFLAGS:=$(COQFLAGS)
 
 COQFLAGS+=$(COQEXTRAFLAGS)
 
+# The following extra flags can probably be removed with Coq 8.21,
+# after Coq pulls https://github.com/coq/coq/pull/19653
+# and/or https://github.com/coq/coq/pull/19981  are merged.
+COQFLAGS+= -w "-notation-incompatible-prefix,-automatic-prop-lowering"
+
 PROFILING?=
 
 ifneq (,$(PROFILING))
diff --git a/fcf b/fcf
index f1bd5f390..291f50057 160000
--- a/fcf
+++ b/fcf
@@ -1 +1 @@
-Subproject commit f1bd5f3903771d78c85ba48f30c6e155aed2b48f
+Subproject commit 291f50057cfbb7c96e58ff11ca9b9f4778467ec1