Merge branch 'master' of https://github.com/math-comp/math-comp

2 files changed, 63 insertions, 5 deletions

diff --git a/etc/ANNOUNCE-1.6.md b/etc/ANNOUNCE-1.6.md
new file mode 100644
index 0000000..a5ad8cb
--- /dev/null
+++ b/etc/ANNOUNCE-1.6.md
@@ -0,0 +1,59 @@
+# Ssreflect/MathComp 1.6 released
+
+We are proud to announce the immediate availability of the
+Ssreflect proof language and the Mathematical Components library
+version 1.6 for Coq 8.4pl6 and 8.5beta3.
+
+This release adds no new theory files.  The proof language 
+received minor fixes while the libraries received minor additions.
+
+A detailed ChageLog is available at:
+  https://github.com/math-comp/math-comp/blob/master/etc/ChangeLog
+Such document contains the list of new theorems as well as the list
+of theorems that were renamed or replaced by more general variants.
+
+The development is now taking place in the public and is mirrored
+on github.  Another announcement specific to this will follow shortly.
+
+The main user visible change is that the library was split into the following components:
+
+  1. ssreflect: Ssreflect proof language, lists, boolean predicates, natural
+     numbers, types with a decidable equality, finite types, finite sets, finite
+     functions, finite graphs, basic arithmetics and prime numbers, big operators
+  2. fingroup: finite groups, group quotients, group morphisms, group
+     presentation, group action
+  3. algebra: discrete algebraic structures as ring, fields, ordered fields,
+     real fields, modules, algebras, vector spaces and integers, rational
+     numbers, polynomials, matrices, vector spaces
+  4. solvable: more definitions and theorems about finite groups
+  5. field: field extensions, Galois theory, algebraic numbers, cyclotomic
+     polynomials
+  6. character: group representations, characters and class functions
+
+A user not needing the entire library can build only the components she is
+interested in.  Each component comes with a file one can Require and Import to
+load, at once, the entire component.
+For example "Require Import all_ssreflect." loads all the theory files in the
+ssreflect component.
+
+The main incompatibility concerning users is the change of logical/physical
+path implied by the reorganization of the library.  In particular "Require
+Ssreflect.ssreflect" does not work anymore.  We propose a schema that is
+compatible with both Coq 8.4 and Coq 8.5, namely:
+  Require Import mathcomp.ssreflect.ssreflect.
+  From mathcomp Require Import ssrfun ssrbool ...
+The first line loads the ssreflect plugin using its full path.
+Then all other files are loaded from the mathcomp name space.
+The component part (like ssreflect or algebra) is omitted.  All theory files in
+the library follow this schema.
+Note that the From directive has effect only in Coq 8.5.  Coq 8.4 ignores it
+and searches for files in all known paths.  Beware of name collisions.
+
+The tarball can be download at the following URL:
+  http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz
+
+The html documentation of the theory files can be browsed at:
+  http://ssr.msr-inria.inria.fr/doc/mathcomp-1.6/
+
+-- The Mathematical Components team
+
diff --git a/etc/INSTALL.md b/etc/INSTALL.md
index f4b4f7b..83b4252 100644
--- a/etc/INSTALL.md
+++ b/etc/INSTALL.md
@@ -1,7 +1,7 @@
 # INSTALLATION PROCEDURE
 
-Users familiar with OPAM can use such tool to install Coq and the Mathematical
-Components library with commands like `opam coq-mathcomp-fingroup`.
+Users familiar with OPAM can use such tool to install Coq and the Mathematical Components library with commands like
+`opam coq-mathcomp-fingroup`.
 
 This document is for users that installed Coq in another way, for example
 compiling it from sources.
@@ -13,15 +13,14 @@ Coq version 8.4pl6 or 8.5 (at the time of writing, beta3)
 ## BUILDING
 
 The Mathematical Components library is divided into various installation
-units.  On can install the entire library (compilation time is XX) or only
-some of its units.
+units.  On can install the entire library (compilation time is around 35 minutes) or only some of its units.
 
 In both cases, if Coq is not installed such that its binaries like `coqc`
 and `coq_makefile` are in the PATH, then the COQBIN environment variable
 must be set to point to the directory containing such binaries.
 For example:
 
-    export COQBIN=/home/gares/coq/bin/
+    export COQBIN=/home/user/coq/bin/
 
 Now, to install the entire library, including the SSReflect proof language: