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. 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
	  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

	* Statements that changed:
	  orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr,
	  cfAut_char, cfConjC_char, invg_lcosets, lcoset_transl,
	  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

	* New theorems:
	  orbit_in_eqP, cards_draws, cfAut_lin_char, cfConjC_lin_char,
	  extend_cfConjC_subset, isometry_of_free, cfAutK, cfAutVK,
	  lcoset_eqP, rcoset_eqP, class_eqP, gFsub_trans, gFnorms,
	  gFchar_trans, gFnormal_trans, gFnorm_trans, mem2_seq1,
	  dvdn_fact, prime_above, subKr, subrI, subIr, subr0_eq,
	  divrI, divIr, divKr, divfI, divIf, divKf, impliesP, impliesPn,
	  unlessL, unlessR, unless_sym, unlessP (coercion), classicW,
	  ltr_prod_nat

	* New notation: "\unless C, P"

12/03/2014 - split the archive in SSReflect and MathComp - version 1.5
	* With this release "ssreflect" has been split into two packages.
	  The Ssreflect one contains the proof language (plugin for Coq) and a
	  small set of core theory libraries about boolean, natural numbers,
	  sequences, decidable equality  and finite types. The Mathematical
	  Components one contains advanced theory files covering a wider
	  spectrum of mathematics.

	* With respect to version 1.4 the proof language got a few new
	  features related to forward reasoning and some bugfixes. The
	  Mathematical Components library features 16 new theory files and in
	  particular: some field and Galois theory, advanced character theory
	  and a construction of algebraic numbers.

05/09/2012 - ssreflect - version 1.4
	* With this release the plugin code received many bug fixes and the
	  existing libraries relevant updates.  This release also includes
	  some new libraries on the following topics: rational numbers,
	  divisibility of integers, F-algebras, finite dimensional field
	  extensions and Euclidean division for polynomials over a ring.

	* The release includes a major code refactoring of the plugin for Coq
	  8.4.  In particular a documented ML API to access the pattern matching
	  facilities of Ssreflect from third party plugins has been introduced.

14/03/2011 - ssreflect - version 1.3
	* The tactic language has been extended with several new features,
	  inspired by the five years of intensive use in our project. However we
	  have kept the core of the language unchanged; the new library compiles
	  with Ssreflect 1.2.  Users of a Coq 8.2 toplevel statically linked
	  with Ssreflect 1.2 need to comment the Declare ML Module "ssreflect"
	  line in ssreflect.v to properly compile the 1.3 library.  We will
	  continue supporting new releases of Coq in due course.

	* The new library adds general linear algebra (matrix rank, subspaces)
	  and all of the advanced finite group that was developed in the course
	  of completing the Local Analysis part of the Odd Order Theorem,
	  starting from the Sylow and Hall theorems and including full structure
	  theorems for abelian, extremal and extraspecial groups, and general
	  (modular) linear representation theory.

14/08/2009 - ssreflect - version 1.2
	* No change log

18/03/2008 - ssreflect - version 1.1
	* First public release