aboutsummaryrefslogtreecommitdiffstats
path: root/INSTALL.md
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2021-01-13 16:53:23 +0100
committerChantal Keller <Chantal.Keller@lri.fr>2021-01-13 16:53:23 +0100
commit68ca86514065cef3d5fc6ce54a86ef15452d8f0a (patch)
treed4f07935f8a2770489435de4d5f853d8d1d4e74f /INSTALL.md
parenta3e412edf10a3a6ef9b352a25c8e62c5fed82538 (diff)
downloadsmtcoq-68ca86514065cef3d5fc6ce54a86ef15452d8f0a.tar.gz
smtcoq-68ca86514065cef3d5fc6ce54a86ef15452d8f0a.zip
Version of OCaml
Diffstat (limited to 'INSTALL.md')
-rw-r--r--INSTALL.md4
1 files changed, 2 insertions, 2 deletions
diff --git a/INSTALL.md b/INSTALL.md
index 84249c4..eb90daf 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -74,12 +74,12 @@ Then follow the instructions of the previous section.
### Requirements
-You need to have OCaml version >= 4.09.0 and Coq version 8.10.*.
+You need to have OCaml version >= 4.08 and < 4.10 and Coq version 8.10.*.
> **Warning**: The version of Coq that you plan to use must have been compiled
> with the same version of OCaml that you are going to use to compile
> SMTCoq. In particular this means you want a version of Coq that was compiled
-> with OCaml version >= 4.09.0.
+> with OCaml version >= 4.08.
If you want to use SMTCoq with high performance to check large proof
certificates, you need to use the [version of Coq with native