porting ChangeLog to Markdown format (#322)

1 files changed, 0 insertions, 271 deletions

diff --git a/ChangeLog b/ChangeLog
deleted file mode 100644
index 16d1102..0000000
--- a/ChangeLog
+++ /dev/null
@@ -1,271 +0,0 @@
-??/??/???? - version 1.7.1
-
-	* Removed `_ : Type` field from packed classes. This performance
-	  optimization is not strictly necessary with modern Coq versions.
-
-	* Added companion matrix of a polynomial `companionmx p` and the
-	  theorems: companionmxK, map_mx_companion and companion_map_poly.
-
-	* Extended generic theory about monotonocity (*mono* and *homo* lemmas).
-
-	* Added: homoW_in, inj_homo_in, mono_inj_in, anti_mono_in,
-	  total_homo_mono_in, homoW, inj_homo, monoj, anti_mono,
-	  total_homo_mono.
-
-	* Extended theory about homo and mono for leq/or and Num.le
-
-	* Changed and extended theory of lersif and intervals:
-	  * Many lersif related lemmas are ported from ssrnum
-	  * Definitions that changed: prev_of_itv, itv_decompose, and itv_rewrite
-	  * Theory of intersections of intervals is added
-
-	* Renamed: (together with the _in suffix counterpart)
-	  mono_inj -> incr_inj
-	  nmono_inj -> decr_inj
-	  leq_mono_inj -> incnr_inj
-	  leq_nmono_inj -> decnr_inj
-	  homo_inj_ltn_lt -> incnr_inj
-	  nhomo_inj_ltn_lt -> decnr_inj
-	  homo_inj_in_lt -> inj_homo_ltr_in
-	  nhomo_inj_in_lt -> inj_nhomo_ltr_in
-	  ltn_ltrW_homo -> ltnrW_homo
-	  ltn_ltrW_nhomo -> ltnrW_nhomo
-	  leq_lerW_mono -> lenrW_mono
-	  leq_lerW_nmono -> lenrW_nmono
-	  homo_leq_mono -> lenr_mono
-	  nhomo_leq_mono -> lenr_nmono
-	  homo_inj_lt -> inj_homo_ltr
-	  nhomo_inj_lt -> inj_nhomo_ltr
-	  homo_inj_ltn_lt -> inj_homo_ltnr
-	  nhomo_inj_ltn_lt -> inj_nhomo_ltnr
-	  homo_mono -> ler_mono
-	  nhomo_mono -> ler_nmono
-
-	* Added sorted_lt_nth, ltn_index, sorted_le_nth, leq_index.
-
-	* Generalized extremum_spec and its theory, added extremum and
-	  extremumP, generalizing arg_min for an arbitrary eqType with an
-	  order relation on it (rather than nat). Redefined arg_min and
-	  arg_max with it.
-
-	* Added [arg minr_( i < n | P ) F] and [arg maxr_( i < n | P ) F]
-	  with all their variants, following the same convention as for nat.
-
-	* Added missing contra* lemma: contra_neqN, contra_neqF,
-	  contra_neqT, contra_neq_eq, contra_eq_neq.
-
-	* Addded missing seq theorems: take_subseq, drop_subseq
-
-	* Reshuffled theorems inside files and packages:
-	  * countalg goes from the field to the algebra package
-	  * finalg now gets inheritance from countalg
-	  * closed_field now contains the construction of algebraic closure
-	    for countable fields that used to be in countalg.
-
-        * Rewritten proof of quantifier elimination for closed field in a
-	  monadic style.
-
-	* Added all_iff, "the following are all equivalent"
-	  with notation [<-> P0; P1; ..; Pn] and theorems
-	  `all_iffLR` and coercion `all_iffP` (see header for doc)
-	  proved by circular implication P0 -> P1 -> ... -> Pn -> P0
-
-	* Removed duplicated definitions of `tag` `tagged` and `Tagged`
-	  from eqtype.v. They were already in ssrfun.v.
-
-	* Specialized `bool_irrelevance` so that the statement reflects
-	  the name.
-
-	* Changed the shape of the type of FieldMixin to allow one-line
-	  in-proof definition of bespoke fieldType structure.
-
-	* Refactored and extended Arguments directives to provide more
-	  comprehensive signature information.
-
-	* Added maximal implicits to reflection, injectivity and cancellation
-	  lemmas so that they are easier to pass to combinator lemmas such as
-	  sameP, inj_eq or canLR.
-
-	* Added reindex_inj s shorthand for reindexing a bigop with a
-	  permutation s.
-
-	* Added lemma `eqmxMunitP`: two matrices with the same shape
-	  represent the same subspace iff they differ only by a change of
-	  basis.
-
-	* Corrected implicits and documentation of MatrixGenField.
-
-	* Renamed `big_setIDdep` to `big_setIDcond`
-	  and `sum_nat_dep_const` to `sum_nat_cond_const`
-
-	* Added lemmas `big_imset_cond`,`big_map_id`, `big_image_cond`
-	  `big_image`, `big_image_cond_id` and `big_image_id` for
-	  completeness purposes
-
-	* Added lemmas `foldrE`, `foldlE`, `foldl_idx` and `sumnE`
-	  to turn "seq statements" into "bigop statements"
-
-	* Generalized the notation `[seq E | i <- s, j <- t]` to the case
-	  where `t` may depend on `i`. The notation is now primitive and
-	  expressed using `flatten` and `map` (see documentation of seq).
-	  `allpairs` now expands to this notation when fully applied.
-	  Added `allpairs_dep` and made it self-expanding as well.
-	  Generalized some lemmas in a backward compatible way.
-	  Some strictly more general lemmas now have suffix `_dep`.
-
-	* Generalised {ffun A -> R} to handle dependent functions, and to be
-	  structurally positive so it can be used in recursive inductive type
-	  definitions. Minor backward incompatibilities: fgraph f is no longer
-	  a field accessor, and no longer equal to val f as {ffun A -> R} is no
-	  longer a subType; some instances of finfun, ffunE, ffunK may not unify
-	  with a generic nondependent function type A -> ?R due to a bug in
-	  Coq < 8.10.
-
-24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
-
-	* Added compatibility with Coq 8.8 and lost compatibility with
-	  Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8.
-
-	* Integration to Coq: ssrbool.v ssrfun.v and plugin.
-	  ssrtest also moved to Coq test suite.
-
-	* Cleaning up the github repository: the math-comp repository is
-	  now dedicated to the released material (as in the present
-	  release). For instance, directories real-closed and odd-order now
-	  have their own repository.
-
-	* Library refactoring: algC ssrnum: Library ssrnum.v now
-	  provides an interface numClosedFieldType, which abstracts the
-	  theory of algebraic numbers. In particular, Re, Im, 'i,
-	  conjC, n.-root and sqrtC, previously defined in library algC.v,
-	  are now part of this generic interface. In case of ambiguity,
-	  a cast to type algC, of complex algebraic numbers, can be used to
-	  disambiguate via  typing constraints. Some theory was thus made
-	  more generic, and the corresponding lemmas, previously defined in
-	  library algC.v (e.g. conjCK) now feature an extra, non maximal
-	  implicit, parameter of type numClosedFieldType. This could break
-	  some proofs.
-
-	* Lemma dvdn_fact was moved from library prime.v to library div.v
-
-	* Structures, changes in interfaces:
-	  numClosedFieldType
-
-	* New Theorems:
-	  iter_in, finv_in, inv_f_in, finv_inj_in, fconnect_sym_in,
-	  iter_order_in, iter_finv_in, cycle_orbit_in, fpath_finv_in,
-	  fpath_finv_f_in, fpath_f_finv_in
-	  big_allpairs
-	  uniqP, uniqPn
-	  dec_factor_theorem,
-	  mul_bin_down, mul_bin_left
-          abstract_context (now merged in Coq)
-
-	* Renamed/generalized:
-	  mul_Sm_binm -> mul_bin_diag
-	  divn1 -> divz1 (in intdiv)
-	  rootC -> nthroot
-	  algRe -> Re
-	  algIm -> Im
-	  algCi -> imaginaryC
-  	  reshape_index_leq -> reshape_leq
-	  Every theorem from ssrnum that used to be in algC
-
-	* Generalized or improved:
-	  ltngtP, contra_eq, contra_neq, odd_opp, nth_iota
-
-24/11/2015 - major reorganization of the archive - version 1.6
-
-	* Files split into sub-directories: 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.
-
-	* Renaming 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 bug fixes. 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