move etc/ files to the root and remove obsolete ones

1 files changed, 0 insertions, 141 deletions

diff --git a/etc/ChangeLog b/etc/ChangeLog
deleted file mode 100644
index 12d6ef4..0000000
--- a/etc/ChangeLog
+++ /dev/null
@@ -1,141 +0,0 @@
-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