diff --git a/INSTALL.md b/INSTALL.md
index 7da6538df7..98e5958b80 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -5,23 +5,27 @@
 - [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 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.
+These requirements can be installed in a custom way, or through
+[opam](https://opam.ocaml.org/) (the recommended way) 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`.
 
-Detailed instructions for possible installations of Mathematical Components are located [here](https://github.com/math-comp/math-comp/blob/master/INSTALL.md).
+Detailed instructions for possible installations of Mathematical Components are located
+[here](https://github.com/math-comp/math-comp/blob/master/INSTALL.md).
 
 ## Short Instructions
 - Through opam:
-  + 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 `opam install coq-mathcomp-analysis.X.Y.Z` where `X.Y.Z` is the version number
+    (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.0, 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
+
 1. Install opam
 - any linux system:
 ```
@@ -30,22 +34,18 @@ $ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/instal
 
 2. Configure opam
 ```
-$ export OPAMROOT=~/.opam_mathcomp_analysis
+$ export OPAMROOT=~/.opam_mathcomp_analysis # opam configuration, metadata, logs, temporary directories and caches
 $ 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,
+To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.3.0
+$ opam install coq-mathcomp-analysis.0.3.1
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
@@ -54,18 +54,22 @@ $ eval `opam config env`
 ```
 
 ### How to edit and test the source code
-If you would rather edit and test the files than intalling them, we suggest that you replace `opam install coq-mathcomp-analysis` command with the following
+
+If you would rather edit and test the files than intalling them, we suggest that you replace
+`opam install coq-mathcomp-analysis` command with the following
 ```
 $ opam install coq-mathcomp-analysis --deps-only
 $ git clone https://github.com/math-comp/analysis
 $ cd analysis
 $ 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)
+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.
+With the example of Coq 8.9.1 and MathComp 1.11.0. For more recent versions, update the
+version numbers accordingly.
 
 1. Install Coq 8.9.1
 ```
@@ -73,16 +77,16 @@ $ opam install coq.8.9.1
 ```
 2. Install Mathematical Components development version 
 ```
-$ opam install coq-mathcomp-ssreflect.1.8.0
-$ opam install coq-mathcomp-fingroup.1.8.0
-$ opam install coq-mathcomp-algebra.1.8.0
-$ opam install coq-mathcomp-solvable.1.8.0
-$ opam install coq-mathcomp-field.1.8.0
+$ opam install coq-mathcomp-ssreflect.1.11.0
+$ opam install coq-mathcomp-fingroup.1.11.0
+$ opam install coq-mathcomp-algebra.1.11.0
+$ opam install coq-mathcomp-solvable.1.11.0
+$ opam install coq-mathcomp-field.1.11.0
 $ opam install coq-mathcomp-bigenough.1.0.0
 ```
 3. Install Finite maps library
 ```
-$ opam install coq-mathcomp-finmap.1.2.0
+$ opam install coq-mathcomp-finmap.1.5.0
 ```
 4. Download and compile `coq-mathcomp-analysis` without installing
 ```
@@ -95,7 +99,8 @@ $ make
 ```
 $ opam remove coq-mathcomp-analysis
 ```
-- However if you wish to clean the entire installation (including `coq` and `mathcomp` dependencies) you should remove the opam root we created for this purpose:
+- However if you wish to clean the entire installation (including `coq` and `mathcomp` dependencies)
+  you should remove the opam root we created for this purpose:
 ```
 $ rm -rf ~/.opam_mathcomp_analysis
 ```