update to last version

INSTALL.md

@@ -1,21 +1,24 @@
 # Installing
 
 ## Requirements
-- [The Coq Proof Assistant version ≥ 8.8](https://coq.inria.fr)
-- [Mathematical Components version ≥ 1.8.0](https://github.com/math-comp/math-comp)
-- [Bigenough version 1.0.0](https://github.com/math-comp/bigenough)
-- [Finmap library version 1.2.0](https://github.com/math-comp/finmap)
+- [The Coq Proof Assistant version ≥ 8.7](https://coq.inria.fr)
+- [Mathematical Components version ≥ 1.11.0](https://github.com/math-comp/math-comp)
+- [Finmap library version ≥ 1.5.0](https://github.com/math-comp/finmap)
 
-These requirements can be installed in a custom way or through [opam 2](https://opam.ocaml.org/) using the repository https://coq.inria.fr/opam/released, which you can add by typing `opam repo add coq-released https://coq.inria.fr/opam/released`.
+These requirements can be installed through [opam](https://opam.ocaml.org/) (the recommended way) using
+- the repository https://coq.inria.fr/opam/extra-dev, if the requirements involve beta releases (as of [2020-06-05] this is the case for MathComp 1.11.0)
+- or, for other versions, the repository https://coq.inria.fr/opam/released, which you can add by typing `opam repo add coq-released https://coq.inria.fr/opam/released`
+or can be installed in a custom way.
 
 Detailed instructions for possible installations of Mathematical Components are located [here](https://github.com/math-comp/math-comp/blob/master/INSTALL.md).
 
 ## Short Instructions
-- Custom (assuming Coq ≥ 8.8, Mathematical Components version ≥ 1.8.0, Bigenough version 1.0.0 and Finmap version 1.2.0 have been installed):
-  + Type `make` to use the provided `Makefile`.
 - Through opam:
-  + Type `opam install coq-mathcomp-analysis`
+  + For the latest version (as of [2020-06-05]), type `opam install coq-mathcomp-analysis.0.3.0` (assuming the `extra-dev` repository has been added)
+  + For other versions, type `opam install coq-mathcomp-analysis`
   (all the dependencies should be automatically installed, assuming `opam` has been properly configured and `coq-released` repository is added)
+- Custom (assuming Coq ≥ 8.7, Mathematical Components version ≥ 1.11, and Finmap version 1.5.0 have been installed):
+  + Type `make` to use the provided `Makefile`.
 
 ## From scratch instructions
 ### How to install as a package
@@ -32,10 +35,18 @@ $ opam init -j4 # adapt to the number of cores you have
 $ eval `opam config env`
 $ opam repo add coq-released https://coq.inria.fr/opam/released
 ```
+To access beta releases:
+```
+$ opam repo add extra-dev https://coq.inria.fr/opam/extra-dev
+```
 3. Install our package (and all its dependencies)
 ```
 $ opam install coq-mathcomp-analysis
 ```
+To install a precise version, type, say 0.3.0,
+```
+$ opam install coq-mathcomp-analysis.0.3.0
+```
 4. Everytime you want to work in this same context, you need to type
 ```
 $ export OPAMROOT=~/.opam_mathcomp_analysis 
@@ -53,6 +64,9 @@ $ make
 You may then browse the files using `coqide` (you might want to `opam install coqide`) or using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
+
+With the example of Coq 8.9.1 and MathComp 1.8.0. For more recent versions, update the version numbers accordingly.
+
 1. Install Coq 8.9.1
 ```
 $ opam install coq.8.9.1