move etc/ files to the root and remove obsolete ones

1 files changed, 141 insertions, 0 deletions

diff --git a/ChangeLog b/ChangeLog
new file mode 100644
index 0000000..12d6ef4
--- /dev/null
+++ b/ChangeLog
@@ -0,0 +1,141 @@
+07/09/2016 - compatibility with Coq 8.7 and several small fixes -
+	version 1.6.2 and upcomming version 1.7
+	* Compatibility with Coq 8.7
+	* Lost compatibility with Coq 8.4
+
+07/09/2016 - compatibility with Coq 8.7 and several small fixes -
+	upcomming version 1.7
+	* New Theorems:
+	   dec_factor_theorem, abstract_context,
+	   mul_bin_down, mul_bin_left
+
+	* Renamings or replacements:
+	  mul_Sm_binm -> mul_bin_diag
+	  divn1 -> divz1 (in intdiv)
+
+	* Generalized or extended:
+	  ltngtP, contra_eq, contra_neq, odd_opp
+
+	* Plugin:
+	  ssrpattern: compose nicely with Tactic Notation
+
+25/08/2016 - refactoring of algC and complex in ssrnum -
+	upcomming version 1.7
+	* ssrnum's interface numClosedFieldType factors some theory from
+	  both complex and algC. Because of that Re, Im, 'i, conjC, n.-root
+	  and sqrtC are not specialized to algC anymore. In case of
+	  ambiguity, they should be instanciated with algC using typing
+	  constraints. Moreoever all the lemmas from ssrnum that used to
+	  be in algC (like conjCK), now take an extra nonmaximal implicit
+	  argument (C : numClosedFieldType) which could break some proofs.
+	  Additionally, ad-hoc constructions from complex.v like -*+ or
+	  complex.Re are now deprecated and one should rely solely on the
+	  ssrnum interface. The next revision might definietly hide those
+	  constructions under a module.
+
+	* Structures that change:
+	  numClosedFieldType
+
+	* Renamed and generalized definitions:
+	  rootC -> nthroot
+	  algRe -> Re
+	  algIm -> Im
+	  algCi -> imaginaryC
+
+	* Renamed and generalized theorems:
+	  Every theorem from ssrnum that used to be in algC
+
+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