diff options
Diffstat (limited to 'INSTALL.md')
-rw-r--r-- | INSTALL.md | 28 |
1 files changed, 13 insertions, 15 deletions
@@ -6,26 +6,12 @@ SMTCoq is designed to work on computers equipped with a POSIX (Unix or a clone) operating system. It is known to work under GNU/Linux (i386 and amd64). -You have various ways to install it: -- the simplest one is via opam; -- you can also install it from the sources, using two different versions +You can install it from the sources, using two different versions of Coq (depending on the efficiency you want). In either case, you will also need to install the provers you want to use (see below). -## Installation via opam (uses Coq-8.5) - -Simply add the coq-extra-dev repo to opam: -``` -opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -``` -and install smtcoq: -``` -opam install coq-smtcoq -``` - - ## Installation from the sources (uses Coq-8.6 or native-coq) You can also build SMTCoq from the sources, using either Coq 8.6 or the @@ -95,6 +81,18 @@ make install ``` +## Deprecated: installation via opam (uses Coq-8.5) + +Simply add the coq-extra-dev repo to opam: +``` +opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev +``` +and install smtcoq: +``` +opam install coq-smtcoq +``` + + ## Installation of the provers To use SMTCoq, you need one or more solvers supported by SMTCoq. |