From cc518c0de948f111e3fcb1b766a1a326db9ce955 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Tue, 6 Mar 2018 12:27:44 +0100
Subject: [doc] Add instructions for dev version installation via OPAM

Plus minor formattig tweaks and typo fixes.
---
 INSTALL.md | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

diff --git a/INSTALL.md b/INSTALL.md
index 9752f0f..d9a74fd 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -3,28 +3,33 @@
 The library is divided into packages which group together related
 files. Each package defines a distribution and compilation unit.
 
-Packages can be compiled using the traditional `make` utility or
-the more recent `OPAM` one. The released and current dev version are
-also available as opam packages.
+Packages can be compiled using the traditional make utility or
+the more recent OPAM one. The released and current dev versions are
+also available as OPAM packages.
 
 ## Compilation and installation of released and current dev version with OPAM
-If you just installed opam you may have to do the following. You may also want
-to read opam user manual first https://opam.ocaml.org/doc/Usage.html
+If you just installed OPAM you may have to do the following. You may also want
+to read [OPAM user manual](https://opam.ocaml.org/doc/Usage.html) first. 
 ```
 opam init
 eval `opam config env`
 ```
-Once your opam envionement is configure you can install any math-comp package via
+Once your OPAM environment is configured
+you can install any math-comp package via
 ```
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam pin add -n coq -k version 8.7.0
 opam install coq -j3
 opam install coq-mathcomp-ssreflect.1.6.4 -j3
 ```
-Replace `ssreflect` here by the package you want, dependencies will be
-installed automatically. You can replace `1.6.4` by `dev` to get the last
-development version. We recommand to pin a particular version of Coq
+Replace `ssreflect` here by the package you want, the dependencies will be
+installed automatically. We recommend pinning a particular version of Coq
 (here `8.7.0`).
+To get the latest development version you need to execute the following:
+```
+opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+opam install coq-mathcomp-ssreflect.dev -j3
+```
 
 ## Compilation and installation with make
 
@@ -34,13 +39,13 @@ The list of Coq versions that are known to work can be obtained with:
 ```
 ls ssreflect/plugin/
 ```
-Alternatively, if you are familiar with the `OPAM` slang:
+Alternatively, if you are familiar with the OPAM slang:
 ```
 grep depends: ssreflect/opam
 ```
 
-If `coqc` is in your `PATH`, then you are good to go.  Alternatively you
-can export the `COQBIN` variable to tell make where the `coqc` binary is:
+If `coqc` is in your `PATH`, then you are good to go.  Alternatively, you
+can export the `COQBIN` variable to tell `make` where the `coqc` binary is:
 ```
 export COQBIN=/home/gares/COQ/coq/bin/
 ```
@@ -62,7 +67,7 @@ To install the compiled library, just execute `make install`.
 ## Compilation and installation of a custom version using OPAM
 
 The instructions assume you are in the `mathcomp` directory
-and that you have `OPAM` installed and configured with the
+and that you have OPAM installed and configured with the
 standard Coq repositories.
 
 For each package, pin the `opam` file:
@@ -79,3 +84,4 @@ For example:
 ```
 opam install coq.8.7.0 coq-mathcomp-ssreflect
 ```
+
-- 
cgit v1.2.3