OPAM currently not supported

1 files changed, 31 insertions, 79 deletions

diff --git a/INSTALL.md b/INSTALL.md
index e384583..9de0b49 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -7,34 +7,45 @@ clone) operating system. It is known to work under GNU/Linux (i386 and
 amd64).
 
 
-## Quick installation
+## Installation from the sources
+
+Currently, SMTCoq can be built only from the sources, using the
+[version of Coq with native data-structures](https://github.com/maximedenes/native-coq). The design of an opam package is under progress.
 
-The simplest way to install SMTCoq is to use the OPAM package, available
-in the
-[Coq unstable repository](https://github.com/coq/repo-unstable.git).
-Once you have OPAM installed on your system:
+1. Download the git version of Coq with native compilation:
+```
+git clone git://github.com/maximedenes/native-coq.git
 ```
-opam repo add coq-stable https://github.com/coq/repo-stable.git
-opam repo add coq-unstable https://github.com/coq/repo-unstable.git
-opam update
-opam install coq coq:smtcoq
+   and compile it by following the instructions available in the
+   repository. We recommand that you do not install it, but only compile
+   it in local:
+```
+./configure -local
+make
 ```
-For more information of opam packages for Coq, see
-[Use OPAM for Coq](http://coq-blog.clarus.me/use-opam-for-coq.html).
 
-This version is sufficient to check small certificates and to solve
-small goals. However, if you want to check larger certificates, we
-recommend using SMTCoq with the
-[version of Coq with native data-structures](https://github.com/maximedenes/native-coq),
-following the instructions in Section "Installation from the sources".
+2. Set an environment variable COQBIN to the directory where Coq's
+   binaries are; for instance:
+```
+export COQBIN=/home/jdoe/native-coq/bin/
+```
+   (the final slash is mandatory).
+
+3. Compile and install SMTCoq by using the commands:
+```
+./configure.sh
+make
+make install
+```
+   in the src directory.
 
 
 ## Installation of the provers
 
-To use SMTCoq, you also need one or more solvers supported by SMTCoq.
+To use SMTCoq, you need one or more solvers supported by SMTCoq.
 Currently, these solvers are:
 
-- [veriT](http://prosecco.gforge.inria.fr/personal/ckeller/Documents-recherche/Smtcoq/verit2c2b43b.tar.gz)
+- [veriT](https://www.lri.fr/~keller/Documents-recherche/Smtcoq/verit2c2b43b.tar.gz)
 
 - [zChaff](http://www.princeton.edu/~chaff/zchaff.html)
 
@@ -47,7 +58,7 @@ proof production mode**, as detailed below.
 ### veriT
 
 The
-[above link](http://prosecco.gforge.inria.fr/personal/ckeller/Documents-recherche/Smtcoq/verit2c2b43b.tar.gz)
+[above link](https://www.lri.fr/~keller/Documents-recherche/Smtcoq/verit2c2b43b.tar.gz)
 points to a snapshot of veriT which is known to be compatible with
 SMTCoq, and is already in proof production mode. If you encounter
 problems to compile it, please report an issue.
@@ -57,68 +68,9 @@ problems to compile it, please report an issue.
 
 zChaff is not actively maintained, so you might encounter problems to
 compile it on modern platforms.
-[This patch](http://prosecco.gforge.inria.fr/personal/ckeller/Documents-recherche/Smtcoq/zchaff64.patch)
+[This patch](https://www.lri.fr/~keller/Documents-recherche/Smtcoq/zchaff64.patch)
 might solve your problems (thanks to Sylvain Boulmé for it); if not,
 please report an issue.
 
 To turn proof production on, you need to uncomment the line
 `// #define VERIFY_ON ` in `zchaff_solver.cpp`.
-
-
-## Installation from the sources
-
-From the sources, SMTCoq can be built either with the standard version
-of Coq or with the
-[version of Coq with native data-structures](https://github.com/maximedenes/native-coq).
-We recommend this latter for efficiency.
-
-
-### With the version of Coq with native data-structures
-
-1. Download the git version of Coq with native compilation:
-```
-git clone git://github.com/maximedenes/native-coq.git
-```
-   and compile it by following the instructions available in the
-   repository. We recommand that you do not install it, but only compile
-   it in local:
-```
-./configure -local
-make
-```
-
-2. Set an environment variable COQBIN to the directory where Coq's
-   binaries are; for instance:
-```
-export COQBIN=/home/jdoe/native-coq/bin/
-```
-   (the final slash is mandatory).
-
-3. Compile and install SMTCoq by using the commands:
-```
-./configure.sh
-make
-make install
-```
-   in the src directory.
-
-
-### With the standard version of Coq
-
-1. Install the standard version of Coq (>= 8.4) by any means that give
-   access to the sources (e.g. via OPAM or from the sources).
-
-2. Set an environment variable COQBIN to the directory where Coq's
-   binaries are; for instance:
-```
-export COQBIN=/home/jdoe/coq-8.4pl5/bin/
-```
-   (the final slash is mandatory).
-
-3. Compile and install SMTCoq by using the commands:
-```
-./configure.sh -standard
-make
-make install
-```
-   in the src directory.