Moved comments on the incompatibility to INSTALL.

Plus added a reference to the issue and the suggested solution in the other
doc files.

3 files changed, 46 insertions, 35 deletions

diff --git a/etc/ANNOUNCE-1.6.md b/etc/ANNOUNCE-1.6.md
index 4f5b1a4..91169ad 100644
--- a/etc/ANNOUNCE-1.6.md
+++ b/etc/ANNOUNCE-1.6.md
@@ -9,8 +9,10 @@ received minor fixes while the libraries received minor additions.
 
 A detailed ChangeLog is available at:
   https://github.com/math-comp/math-comp/blob/master/etc/ChangeLog
-This document contains the list of new theorems as well as the list
-of theorems that were renamed or replaced by more general variants.
+This document contains in particulat the list of new theorems as well
+as the list of theorems that were renamed or replaced by more
+general variants.
+
 
 Our development repository is now public, and mirrored on github:
   https://github.com/math-comp/math-comp
@@ -45,30 +47,15 @@ entire component. For example the command
 loads all the theory files in the contained in the 'ssreflect'
 component.
 
-This modularity comes at the price of an incompatibility for users of
-previous version of the Mathematical Components library, due to the
-change of logical/physical paths implied by the reorganization of the
-library. In particular the command line
-
-         Require Ssreflect.ssreflect.
-
-does not work anymore.  We propose a replacement schema for such
-command lines that is compatible with both versions 8.4 and 8.5 of
-Coq, namely replacing the previous line with:
-
-     Require Import mathcomp.ssreflect.ssreflect.
-
-     From mathcomp Require Import ssrfun ssrbool ...
+Note that this modularity comes at the price of a possible
+incompatibility for users of previous version of the Mathematical
+Components library, due to the change of logical/physical paths
+implied by the reorganization of the library. See the installation
+notes for more on this issue an a suggested migration scheme.
 
-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: hence beware of the
-possible name collisions.
+The tarball can be download at
+http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz
 
-The tarball can be download at 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/
 
diff --git a/etc/ChangeLog b/etc/ChangeLog
index a603a9f..ee28d7d 100644
--- a/etc/ChangeLog
+++ b/etc/ChangeLog
@@ -1,26 +1,28 @@
-24/11/2015 - major reorganization of the archive - version 1.6 
-	* Files split into subdirectories: ssreflect, algebra, fingroup,  
+24/11/2015 - major reorganization of the archive - version 1.6
+	* Files split into subdirectories: ssreflect, algebra, fingroup,
 	  solvable, field and character. In this way the user can decide
 	  to compile only the subset of the Mathematical Components library
-	  that is relevant to her.
+	  that is relevant to her. Note that this introduces a possible
+	  incompatibility for users of the previous version. A replacement
+	  scheme is suggested in the installation notes.
 
 	* The archive is now open and based on git. Public mirror at:
 	         https://github.com/math-comp/math-comp
-	         
-	* Sources of the reference manual of the Ssreflect tactic language are 
+
+	* Sources of the reference manual of the Ssreflect tactic language are
 	  also open and available at:
 		https://github.com/math-comp/ssr-manual
 	  Pull requests improving the documentation are welcome.
-		
+
 	* Renamings or replacements:
 	  conjC_closed -> cfConjC_closed
 	  class_transr -> class_eqP
 	  cfclass_transl -> cfclass_transr
 	  nontrivial_ideal -> proper_ideal
 	  zchar_orthonormalP -> vchar_orthonormalP
-	  
+
 	* Definitions that changed:
-	  seq_sub	
+	  seq_sub
 
 	* Statements that changed:
 	  orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr,
@@ -28,7 +30,7 @@
 	  lcoset_transr, rcoset_transl, rcoset_transr, mem2_last,
 	  bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5,
 	  ltr0_neq0, ltr_prod, Zisometry_of_iso
-	
+
 	* New definitions:
 	  adhoc_seq_sub_choiceMixin, adhoc_seq_sub_[choice|fin]Type
 
@@ -90,4 +92,3 @@
 
 18/03/2008 - ssreflect - version 1.1
 	* First public release
-
diff --git a/etc/INSTALL.md b/etc/INSTALL.md
index 83b4252..0ea3c4c 100644
--- a/etc/INSTALL.md
+++ b/etc/INSTALL.md
@@ -6,7 +6,7 @@ Users familiar with OPAM can use such tool to install Coq and the Mathematical C
 This document is for users that installed Coq in another way, for example
 compiling it from sources.
 
-## REQUIREMENTS 
+## REQUIREMENTS
 
 Coq version 8.4pl6 or 8.5 (at the time of writing, beta3)
 
@@ -75,3 +75,26 @@ file.
 Coq sources have a .v extension. Opening any .v file should
 automatically launch ProofGeneral.
 
+## TRANSITION FROM 1.5 to 1.6
+
+The change of logical/physical paths implied by the reorganization of the
+library causes an incompatibility for users of previous version of the
+Mathematical Components library. For instance the command line
+
+          Require Ssreflect.ssreflect.
+
+does not work anymore.  We propose a replacement schema for such
+command lines that is compatible with both versions 8.4 and 8.5 of
+Coq, namely replacing the previous line with:
+
+          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: hence beware of the
+possible name collisions.