From 9eb0f5ec4e2a1a700d1d5f7985e970a2e59a2cb7 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 6 Feb 2024 18:25:18 -0500 Subject: [PATCH] This repository requires Coq 8.18 or later. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 3b446d0d77..95e2a5d1e8 100644 --- a/README.md +++ b/README.md @@ -30,7 +30,7 @@ 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.17](https://github.com/coq/coq/releases/tag/V8.17.0) or later. +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`. 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.