porting ChangeLog to Markdown format (#322)

2 files changed, 282 insertions, 271 deletions

diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..9a0559c
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,282 @@
+# Changelog
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
+
+## [Unreleased]
+
+Drop compatibility with Coq 8.6 (OCaml plugin removed).
+MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9.
+
+### Added
+
+- Companion matrix of a polynomial `companionmx p` and the
+  theorems: `companionmxK`, `map_mx_companion` and `companion_map_poly`
+  
+- `homoW_in`, `inj_homo_in`, `mono_inj_in`, `anti_mono_in`,
+  `total_homo_mono_in`, `homoW`, `inj_homo`, `monoj`, `anti_mono`,
+  `total_homo_mono`
+
+- `sorted_lt_nth`, `ltn_index`, `sorted_le_nth`, `leq_index`.
+
+- `[arg minr_( i < n | P ) F]` and `[arg maxr_( i < n | P ) F]`
+  with all their variants, following the same convention as for `nat`
+
+- `contra_neqN`, `contra_neqF`, `contra_neqT`, `contra_neq_eq`, `contra_eq_neq`
+
+- `take_subseq`, `drop_subseq`
+
+- `big_imset_cond`,`big_map_id`, `big_image_cond`
+  `big_image`, `big_image_cond_id` and `big_image_id`
+
+- `foldrE`, `foldlE`, `foldl_idx` and `sumnE`
+  to turn "seq statements" into "bigop statements"
+
+- `all_iff` with notation `[<-> P0; P1; ..; Pn]` to talk about
+  circular implication `P0 -> P1 -> ... -> Pn -> P0`.
+  Related theorems are `all_iffLR` and `all_iffP`
+
+### Changed
+
+- Theory of `lersif` and intervals:
+  + Many `lersif` related lemmas are ported from `ssrnum`
+  + Changed: `prev_of_itv`, `itv_decompose`, and `itv_rewrite`
+  + New theory of intersections of intervals
+
+- 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.
+
+- Reshuffled theorems inside files and packages:
+  + `countalg` goes from the field to the algebra package
+  + `finalg` inherits from countalg
+  + `closed_field` contains the construction of algebraic closure
+    for countable fields that used to be in countalg.
+
+- Maximal implicits applied 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`.
+
+- Rewritten proof of quantifier elimination for closed field in a
+  monadic style.
+
+- 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.
+
+- 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 version 8.9 or below.
+
+### Renamed
+
+Renamings also involve the `_in` suffix counterpart when applicable
+
+- `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`
+- `big_setIDdep` -> `big_setIDcond`
+- `sum_nat_dep_const` -> `sum_nat_cond_const`
+
+### Misc
+
+- Removed trailing `_ : Type` field from packed classes. This performance
+  optimization is not strictly necessary with modern Coq versions.
+
+- Removed duplicated definitions of `tag`, `tagged` and `Tagged`
+  from `eqtype.v`. They are already in `ssrfun.v`.
+
+## [1.7.0] - 2018-04-24
+
+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 in Coq startng from version 8.7 of:
+  + OCaml plugin (plugin for 8.6 still in the archive for backward compatibility)
+  + `ssreflect.v`, `ssrbool.v`, `ssrfun.v` and `ssrtest/`
+
+- 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.
+
+### Changed
+
+- Library refactoring: `algC` and `ssrnum`.
+  Library `ssrnum.v` 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.
+  Every theorem from `ssrnum` that used to be in `algC` changed statement.
+  
+- `ltngtP`, `contra_eq`, `contra_neq`, `odd_opp`, `nth_iota`
+
+### Added
+
+- `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` (`in ssreflect.v`, now merged in Coq proper)
+
+### Renamed
+
+- Lemma `dvdn_fact` was moved from library `prime.v` to library `div.v`
+- `mul_Sm_binm -> mul_bin_diag
+- `divn1` -> `divz1` (in intdiv)
+- `rootC` -> `nthroot`
+- `algRe` -> `Re`
+- `algIm` -> `Im`
+- `algCi` -> `imaginaryC`
+- `reshape_index_leq` -> `reshape_leq`
+
+## [1.6.0] - 2015-11-24 (ssreflect + mathcomp)
+
+Major reorganization of the archive.
+
+- 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.
+
+### Renamed
+- `conjC_closed` -> `cfConjC_closed`
+- `class_transr` -> `class_eqP`
+- `cfclass_transl` -> `cfclass_transr`
+- `nontrivial_ideal` -> `proper_ideal`
+- `zchar_orthonormalP` -> `vchar_orthonormalP`
+
+### Changed
+- `seq_sub`
+- `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`
+
+### Added
+- `adhoc_seq_sub_choiceMixin`, `adhoc_seq_sub_[choice|fin]Type`
+- `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`
+- Notation `\unless C, P`
+
+## [1.5.0] - 2014-03-12 (ssreflect + mathcomp)
+
+Split the archive in SSReflect and MathComp
+
+- 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.
+
+## [1.4.0] - 2012-09-05 (ssreflect)
+
+- 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.
+
+## [1.3.0] - 2011-03-14 (ssreflect)
+
+- 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.
+
+## [1.2.0] - 2009-08-14 (ssreflect)
+
+No change log
+
+## [1.1.0] - 2008-03-18 (ssreflect)
+
+First public release
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