add coq-mathcomp-classical to install instructions (#88)

installation.org

@@ -10,13 +10,24 @@
 #+HTML_HEAD: <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
 #+HTML_HEAD: <style type="text/css"> body { max-width: 1100px; width: 100% - 30px; margin-left: 30px; }</style>
 
+The Mathematical Components libraries are provided as separate packages:
+
+- The base libraries are the libraries that support the formalization
+  of the Four Color Theorem and of the Odd Order Theorem.
+
+- Other libraries contain extensions and applications.
+
+The installation of Mathematical Components is best done using [[https://opam.ocaml.org/][opam]], a
+package manager for [[https://ocaml.org/][OCaml]], the programming language with which [[https://coq.inria.fr/][Coq]] is
+implemented.
+
+The relevant packages can be found in the [[https://coq.inria.fr/opam/www/][Coq package index]];
+their name is usually prefixed with ~coq-mathcomp-~.
+
 * Install the Base Mathematical Components Libraries
 
 ** Installation using the [[https://opam.ocaml.org/][opam]] package manager
 
-- The installation of Mathematical Components can be done using [[https://opam.ocaml.org/][opam]],
-  a package manager for [[https://ocaml.org/][OCaml]], the programming language with which [[https://coq.inria.fr/][Coq]]
-  is implemented.
 - Using opam, the installation of the base Mathematical Components
   library is as simple as this:
 
@@ -26,58 +37,65 @@ opam install coq-mathcomp-ssreflect
 #+END_SRC
 
 - Other base mathematical components libraries can then be installed
-  similarly using ~opam install~. The available packages can be found
-  in the [[https://coq.inria.fr/opam/www/][Coq package index]]:
+  similarly using ~opam install~:
   + ~coq-mathcomp-algebra~,
   + ~coq-mathcomp-field~,
   + ~coq-mathcomp-solvable~,
   + ~coq-mathcomp-fingroup~,
   + ~coq-mathcomp-character~.
 
-- You can find more detailed installation instructions in [[https://github.com/math-comp/math-comp/blob/master/INSTALL.md][INSTALL.md]]
-  (from the official distribution), this includes:
-  + various ways of installing using ~opam~
-  + installation from the source files (using ~make~)
-  + installation using nix
-
 ** Installation using the [[https://github.com/coq/platform][Coq platform]]
 
 - The [[https://github.com/coq/platform][Coq platform]] is a distribution of [[https://coq.inria.fr/][Coq]] together with a selection of libraries
   including most Mathematical Components libraries. It supports Linux, macOS, and Windows.
 
-** Installation Instructions in Other Languages
+** Other installation instructions and details
+
+- You can find more detailed installation instructions in [[https://github.com/math-comp/math-comp/blob/master/INSTALL.md][INSTALL.md]]
+  (from the official distribution), this includes:
+  + various ways of installing using ~opam~
+  + installation from the source files (using ~make~)
+  + installation using nix
 
 - Installation instructions in [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html][Japanese, 日本語]]
   + see「パッケージからの設定」for installation using ~opam~
 
-** Advanced: Installation Instructions for Windows 10 & 11 using cygwin-opam or WSL
+- Advanced: Installation Instructions for Windows 11 using cygwin-opam or WSL
+  + It is possible to install the Mathematical Components libraries on
+    Windows 11 using [[https://www.cygwin.com/][cygwin]] together with the binary distribution of Coq
+    or together with [[https://fdopen.github.io/opam-repository-mingw/installation/][opam for Windows]], or with Windows Subsystem for
+    Linux, as explained for example [[https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org][here]].
+
+* Install Other Mathematical Components Libraries
 
-- It is possible to install the Mathematical Components libraries on
-  Windows 10 & 11 using [[https://www.cygwin.com/][cygwin]] together with the binary distribution of Coq
-  or together with [[https://fdopen.github.io/opam-repository-mingw/installation/][opam for Windows]], or with Windows Subsystem for
-  Linux, as explained for example [[https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org][here]]
+There are several libraries that build on top of the base
+Mathematical Components libraries, e.g.:
 
-* Other Mathematical Components Libraries
+Extensions:
+
+1. [[https://github.com/math-comp/finmap][Finite sets, finite maps, multisets and generic sets]]
+   - Available as the opam package ~coq-mathcomp-finmap~
+2. [[https://github.com/math-comp/multinomials][Multinomials for the Mathematical Components library]]
+   - Available as the opam package ~coq-mathcomp-multinomials~
+3. [[https://github.com/math-comp/real-closed][Theorems for Real Closed Fields]]
+   - Available as the opam package ~coq-mathcomp-real-closed~
+4. A layer for classical reasoning (developed along [[https://github.com/math-comp/analysis][MathComp Analysis]])
+   - Available as the opam package ~coq-mathcomp-classic~
+4. [[https://github.com/math-comp/analysis][MathComp Analysis]]
+   - Available as the opam package ~coq-mathcomp-analysis~
 
-There are already several libraries that build on top of the base
-Mathematical Components libraries:
+Applications:
 
 1. [[https://github.com/math-comp/fourcolor][The Four Color theorem]]
    - Available as the opam package ~coq-fourcolor~
 2. [[https://github.com/math-comp/odd-order][The Odd Order theorem]]
    - Available as the opam package ~coq-mathcomp-odd-order~
-3. [[https://github.com/math-comp/analysis][MathComp Analysis]]
-   - Available as the opam package ~coq-mathcomp-analysis~
-4. [[https://github.com/math-comp/Abel][Abel-Ruffini theorem]]
+3. [[https://github.com/math-comp/Abel][Abel-Ruffini theorem]]
    - Available as the opam package ~coq-mathcomp-abel~
-5. [[https://github.com/math-comp/real-closed][Theorems for Real Closed Fields]]
-   - Available as the opam package ~coq-mathcomp-real-closed~
-6. [[https://github.com/math-comp/finmap][Finite sets, finite maps, multisets and generic sets]]
-   - Available as the opam package ~coq-mathcomp-finmap~
-7. [[https://github.com/math-comp/multinomials][Multinomials for the Mathematical Components library]]
-   - Available as the opam package ~coq-mathcomp-multinomials~
-8. [[https://github.com/coq-community/apery][A formal proof of the irrationality of zeta(3), the Apéry constant]]
+4. [[https://github.com/coq-community/apery][A formal proof of the irrationality of zeta(3), the Apéry constant]]
    - Available as the opam package ~coq-mathcomp-apery~
-9. See the Mathematical Components' [[https://github.com/math-comp][github]] for more libraries.
-   [[https://github.com/coq-community][coq-community]] also features a number of libraries using Mathematical Components.
+
+More libraries:
+- See the Mathematical Components' [[https://github.com/math-comp][github]].
+- [[https://github.com/coq-community][coq-community]] also features a number of libraries using Mathematical Components.