Changelog file created

etc/ChangeLog

@@ -0,0 +1,80 @@
+24/11/2015 - major reorganization of the archive - version 1.6 
+	* Files split into subdirectories: ssreflect, algebra, fingroup,  
+	  solvable, field and character.
+
+	* The archive is now open and based on git. Public mirror at:
+	         https://github.com/math-comp/math-comp
+
+	* Renamings or replacements:
+	  conjC_closed -> cfConjC_closed
+	  class_transr -> class_eqP
+	  cfclass_transl -> cfclass_transr
+	  nontrivial_ideal -> proper_ideal
+	  zchar_orthonormalP -> vchar_orthonormalP
+
+	* 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 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
+