Update installation instructions

1 files changed, 56 insertions, 1 deletions

diff --git a/INSTALL.md b/INSTALL.md
index b0e5c2f..0c2808d 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -13,7 +13,7 @@ You will also need to [install the provers](#installation-of-the-provers)
 you want to use.
 
 
-## Installation via opam (recommended)
+## Installation of version 2.0 via opam (recommended)
 
 ### In an existing switch
 
@@ -21,6 +21,61 @@ You need to have OCaml version >= 4.09 and Coq >= 8.11.
 
 Simply add the coq-extra-dev repo to opam:
 ```bash
+opam repo add coq-released https://coq.inria.fr/opam/released
+```
+and install SMTCoq:
+```bash
+opam install coq-smtcoq
+```
+
+### In a new switch
+
+Create a switch:
+```bash
+opam switch create ocaml-base-compiler.4.09.0
+eval $(opam env)
+```
+add the Coq repos to opam:
+```bash
+opam repo add coq-released https://coq.inria.fr/opam/released
+```
+and install SMTCoq:
+```bash
+opam install coq-smtcoq
+```
+
+### If you are new to opam
+
+We recommended to install the required packages from
+[opam](https://opam.ocaml.org). Once you have installed opam on your system you
+should issue the following command:
+
+```bash
+opam init
+```
+
+which will initialize the opam installation and prompt for modifying the shell
+init file.
+
+Once opam is installed you should still issue
+
+```bash
+eval `opam config env`
+```
+
+(this is not necessary if you start another session in your shell).
+
+Then follow the instructions of the previous section.
+
+
+## Installation of the development version via opam
+
+### In an existing switch
+
+You need to have OCaml version >= 4.09 and Coq 8.13.
+
+Simply add the coq-extra-dev repo to opam:
+```bash
 opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
 ```
 and install SMTCoq: