Require Coq 8.20

Author: andres-erbsen

.github/workflows/coq-macos.yml

@@ -32,7 +32,7 @@ jobs:
 
     env:
       NJOBS: "2"
-      COQ_VERSION: "8.18.0" # pick a version not tested on other platforms
+      COQ_VERSION: "8.20.0"
       COQCHKEXTRAFLAGS: ""
       SKIP_BEDROCK2: "0"
       OPAMYES: "true"

.github/workflows/coq-windows.yml

@@ -26,7 +26,7 @@ jobs:
 
     env:
       NJOBS: "2"
-      COQ_VERSION: "8.18.0" # minimal major version required for bedrock2 components
+      COQ_VERSION: "8.20.0"
       COQEXTRAFLAGS: "-async-proofs-j 1"
       COQCHKEXTRAFLAGS: ""
       OPAMYES: "true"

README.md

@@ -31,8 +31,8 @@ Building
 🌐 Try out synthesis [on the web](https://mit-plv.github.io/fiat-crypto/)!
 (Supported by [`js_of_ocaml`](https://ocsigen.org/js_of_ocaml/latest/manual/overview) compilation.)
 
-This repository requires [Coq](https://coq.inria.fr/) [8.18](https://github.com/coq/coq/releases/tag/V8.18.0) or later.
-Note that if you install Coq from Ubuntu aptitude packages, you need `libcoq-ocaml-dev` in addition to `coq`.
+This repository requires [Coq](https://coq.inria.fr/) 8.20 or later, including OCaml libraries.
+If you install Coq from Ubuntu aptitude packages, you need `libcoq-ocaml-dev` in addition to `coq`.
 Note that in some cases (such as installing Coq via homebrew on Mac), you may also need to install `ocaml-findlib` (for `ocamlfind`).
 The extracted OCaml code for the standalone binaries requires [OCaml](https://ocaml.org/) [4.08](https://ocaml.org/p/ocaml/4.08.0) or later.
 We suggest downloading [the latest version of Coq](https://github.com/coq/coq/wiki#coq-installation).