path: root/CHANGELOG.md

# Changelog
All notable changes to this project will be documented in this file.

Last releases: [[1.12.0] - 2020-11-26](#1120---2020-11-26), [[1.11.0] - 2020-06-09](#1110---2020-06-09), and [[1.10.0] - 2019-11-29](#1100---2019-11-29).

The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).

## [1.12.0] - 2020-11-26

This release is compatible with Coq versions 8.10, 8.11, and 8.12.

### Added

- Contraposition lemmas involving propositions:
  + in `ssrbool.v`: `contra_not`, `contraPnot`, `contraTnot`,
    `contraNnot`, `contraPT`, `contra_notT`, `contra_notN`,
    `contraPN`, `contraFnot`, `contraPF` and `contra_notF`.
  + in `eqtype.v`: `contraPeq`, `contra_not_eq`, `contraPneq`, and
    `contra_neq_not`, `contra_not_neq`, `contra_eq_not`.
- Contraposition lemmas involving inequalities:
  + in `ssrnat.v`: `contraTleq`, `contraTltn`, `contraNleq`,
    `contraNltn`, `contraFleq`, `contraFltn`, `contra_leqT`,
    `contra_ltnT`, `contra_leqN`, `contra_ltnN`, `contra_leqF`,
    `contra_ltnF`, `contra_leq`, `contra_ltn`, `contra_leq_ltn`,
    `contra_ltn_leq`, `contraPleq`, `contraPltn`, `contra_not_leq`,
    `contra_not_ltn`, `contra_leq_not`, `contra_ltn_not`
  + in `order.v`: `comparable_contraTle`, `comparable_contraTlt`,
    `comparable_contraNle`, `comparable_contraNlt`,
    `comparable_contraFle`, `comparable_contraFlt`, `contra_leT`,
    `contra_ltT`, `contra_leN`, `contra_ltN`, `contra_leF`,
    `contra_ltF`, `comparable_contra_leq_le`,
    `comparable_contra_leq_lt`, `comparable_contra_ltn_le`,
    `comparable_contra_ltn_lt`, `contra_le_leq`, `contra_le_ltn`,
    `contra_lt_leq`, `contra_lt_ltn`, `comparable_contra_le`,
    `comparable_contra_le_lt`, `comparable_contra_lt_le`,
    `comparable_contra_lt`, `contraTle`, `contraTlt`, `contraNle`,
    `contraNlt`, `contraFle`, `contraFlt`, `contra_leq_le`,
    `contra_leq_lt`, `contra_ltn_le`, `contra_ltn_lt`, `contra_le`,
    `contra_le_lt`, `contra_lt_le`, `contra_lt`, `contra_le_not`,
    `contra_lt_not`, `comparable_contraPle`, `comparable_contraPlt`,
    `comparable_contra_not_le`, `comparable_contra_not_lt`,
    `contraPle`, `contraPlt`, `contra_not_le`, `contra_not_lt`

- in `ssreflect.v`, added intro pattern ltac views for dup, swap,
  apply: `/[apply]`, `/[swap]` and `/[dup]`.

- in `ssrbool.v` (waiting to be integrated in Coq)
  + generic lemmas about interaction between `{in _, _}` and `{on _,  _}`:
    `in_on1P`, `in_on1lP`, `in_on2P`, `on1W_in`, `on1lW_in`, `on2W_in`,
    `in_on1W`, `in_on1lW`, `in_on2W`, `on1S`, `on1lS`, `on2S`,
    `on1S_in`, `on1lS_in`, `on2S_in`, `in_on1S`, `in_on1lS`, `in_on2S`.
  + lemmas about interaction between `{in _, _}` and `sig`:
    `in1_sig`, `in2_sig`, and `in3_sig`.

- in `ssrnat.v`, new lemmas: `subn_minl`, `subn_maxl`, `oddS`,
  `subnA`, `addnBn`, `addnCAC`, `addnACl`, `iterM`, `iterX`

- in `seq.v`,
  + new lemmas `take_uniq`, `drop_uniq`
  + new lemma `mkseqP` to abstract a sequence `s` with `mkseq f n`,
    where `f` and `n` are fresh variables.
  + new high-order relation `allrel r xs ys` which asserts that
    `r x y` holds whenever `x` is in `xs` and `y` is in `ys`, new notation
    `all2rel r xs (:= allrel r xs xs)` which asserts that `r` holds on all
    pairs of elements of `xs`, and
    * lemmas `allrel0(l|r)`, `allrel_cons(l|r|2)`, `allrel1(l|r)`,
      `allrel_cat(l|r)`, `allrel_allpairsE`, `eq_in_allrel`, `eq_allrel`,
      `allrelC`, `allrel_map(l|r)`, `allrelP`,
    * new lemmas `all2rel1`, `all2rel2`, and `all2rel_cons`
      under assumptions of symmetry of `r`.
  + new lemmas `allss`, `all_mask`, and `all_sigP`.
    `allss` has also been declared as a hint.
  + new lemmas `index_pivot`, `take_pivot`, `rev_pivot`,
    `eqseq_pivot2l`, `eqseq_pivot2r`, `eqseq_pivotl`, `eqseq_pivotr`
    `uniq_eqseq_pivotl`, `uniq_eqseq_pivotr`, `mask_rcons`, `rev_mask`,
    `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, and
    `uniq_subseq_pivot`.
  + new lemmas `find_ltn`, `has_take`, `has_take_leq`,
    `index_ltn`, `in_take`, `in_take_leq`, `split_find_nth`,
    `split_find` and `nth_rcons_cat_find`.
  + added `drop_index`, `in_mask`, `mask0s`, `cons_subseq`,
    `undup_subseq`, `leq_count_mask`, `leq_count_subseq`,
    `count_maskP`, `count_subseqP`, `count_rem`, `count_mem_rem`,
    `rem_cons`, `remE`, `subseq_rem`, `leq_uniq_countP`, and
    `leq_uniq_count`.
  + new definition `rot_add` and new lemmas `rot_minn`,
    `leq_rot_add`, `rot_addC`, `rot_rot_add`.
  + new lemmas `perm_catACA`, `allpairs0l`, `allpairs0r`,
    `allpairs1l`, `allpairs1r`, `allpairs_cons`, `eq_allpairsr`,
    `allpairs_rcons`, `perm_allpairs_catr`, `perm_allpairs_consr`,
    `mem_allpairs_rconsr`, and `allpairs_rconsr` (with the alias
    `perm_allpairs_rconsr` for the sake of uniformity, but which is
    already deprecated in favor of `allpairs_rconsr`, cf renamed
    section).

- in `path.v`,
  + new lemmas `sub_cycle(_in)`, `eq_cycle_in`,
    `(path|sorted)_(mask|filter)_in`, `rev_cycle`, `cycle_map`,
    `(homo|mono)_cycle(_in)`.
  + new lemma `sort_iota_stable`.
  + new lemmas `order_path_min_in`, `path_sorted_inE`,
    `sorted_(leq|ltn)_nth_in`, `subseq_path_in`, `subseq_sorted_in`,
    `sorted_(leq|ltn)_index_in`, `sorted_uniq_in`, `sorted_eq_in`,
    `irr_sorted_eq_in`, `sort_sorted_in`, `sorted_sort_in`, `perm_sort_inP`,
    `all_sort`, `sort_stable_in`, `filter_sort_in`, `(sorted_)mask_sort_in`,
    `(sorted_)subseq_sort_in`, and `mem2_sort_in`.
  + added `size_merge_sort_push`, which documents an
    invariant of `merge_sort_push`.

- in `fintype.v`,
  + new lemmas `card_geqP`, `card_gt1P`, `card_gt2P`, `card_le1_eqP`
    (generalizes `fintype_le1P`),
  + adds lemma `split_ordP`, a variant of `splitP` which introduces
    ordinal equalities between the index and `lshift`/`rshift`, rather
    than equalities in `nat`, which in some proofs makes the reasoning
    easier (cf `matrix.v`), especially together with the new lemma
    `eq_shift` (which is a multi-rule for new lemmas `eq_lshift`,
    `eq_rshift`, `eq_lrshift` and `eq_rlshift`).
  + new lemmas `eq_liftF` and `lift_eqF`.
  + new lemmas `disjointFr`, `disjointFl`, `disjointWr`, `disjointW`
  + new (pigeonhole) lemmas `leq_card_in`, `leq_card`,
  + added `mask_enum_ord`.

- in `finset.v`
  + new lemmas `set_enum`, `cards_eqP`, `cards2P`
  + new lemmas `properC`, `properCr`, `properCl`
  + new lemmas `mem_imset_eq`, `mem_imset2_eq`. These lemmas will
    lose the `_eq` suffix in the next release, when the shortende
    names will become available (cf. Renamed section)
  + new lemma `disjoints1`

- in `order.v`
  + new lemmas `comparable_bigl` and `comparable_bigr`.
  + added a factory `distrLatticePOrderMixin` to build a
    `distrLatticeType` from a `porderType`.
  + new notations `0^d` and `1^d` for bottom and top elements of dual
    lattices.
  + new definition `lteif` and notations `<?<=%O`, `<?<=^d%O`, `_ < _ ?<= if _`,
    and `_ <^d _ ?<= if _` (cf Changed section).
  + new lemmas `lteifN`, `comparable_lteifNE`, and
    `comparable_lteif_(min|max)(l|r)`.

- in `bigop.v`,
  + new lemma `sig_big_dep`, analogous to `pair_big_dep`
    but with an additional dependency in the index types `I` and `J`.
  + new lemma `reindex_omap` generalizes `reindex_onto`
    to the case where the inverse function to `h` is partial (i.e. with
    codomain `option J`, to cope with a potentially empty `J`.
  + new lemma `bigD1_ord` takes out an element in the
    middle of a `\big_(i < n)` and reindexes the remainder using `lift`.
  + new lemma `big_uncond`. The ideal name is `big_rmcond`
    but it has just been deprecated from its previous meaning (see
    Changed section) so as to reuse it in next mathcomp release.
  + new lemma `big_uncond_in` is a new alias of
    `big_rmcond_in` for the sake of uniformity, but it is already
    deprecated and will be removed two releases from now.
  + added `big_mask_tuple` and `big_mask`.

- in `fingraph.v`, new lemmas `fcard_gt0P`, `fcard_gt1P`

- in `perm.v`, new lemma `permS01`.

- in `ssralg.v`
  + new lemmas `sumr_const_nat` and `iter_addr_0`
  + new lemmas `iter_addr`, `iter_mulr`, `iter_mulr_1`, and
    `prodr_const_nat`.
  + new lemma `raddf_inj`, characterizing injectivity for additive
    maps.
  + Lemma `expr_sum` : equivalent for ring of `expn_sum`
  + Lemma `prodr_natmul` : generalization of `prodrMn_const`. Its name
    will become `prodrMn` in the next release when this name will
    become available (cf. Renamed section).

- in `poly.v`, new lemma `commr_horner`.

- in `polydiv.v`, new lemma `dvdpNl`.

- in `matrix.v`,
  + new definitions `is_diag_mx` and `is_trig_mx` characterizing
    respectively diagonal and lower triangular matrices.  We provide
    the new lemmas `row_diag_mx`, `is_diag_mxP`, `diag_mxP`,
    `diag_mx_is_diag`, `mx0_is_diag`, `is_trig_mxP`,
    `is_diag_mx_is_trig`, `diag_mx_trig`, `mx0_is_trig`,
    `scalar_mx_is_diag`, `is_scalar_mx_is_diag`, `scalar_mx_is_trig`
    and `is_scalar_mx_is_trig`.
  + new lemmas `matrix_eq0`, `matrix0Pn`, `rV0Pn` and `cV0Pn` to
    characterize nonzero matrices and find a nonzero coefficient.
  + new predicate `mxOver S` qualified with `\is a`, and
    * new lemmas `mxOverP`, `mxOverS`, `mxOver_const`,
      `mxOver_constE`, `thinmxOver`, `flatmxOver`, `mxOver_scalar`,
      `mxOver_scalarE`, `mxOverZ`, `mxOverM`, `mxOver_diag`,
      `mxOver_diagE`.
    * new canonical structures:
      - `mxOver S` is closed under addition if `S` is.
      - `mxOver S` is closed under negation if `S` is.
      - `mxOver S` is a sub Z-module if `S` is.
      - `mxOver S` is a semiring for square matrices if `S` is.
      - `mxOver S` is a subring for square matrices if `S` is.
  + new lemmas about `map_mx`: `map_mx_id`, `map_mx_comp`,
    `eq_in_map_mx`, `eq_map_mx` and `map_mx_id_in`.
  + new lemmas `row_usubmx`, `row_dsubmx`, `col_lsubmx`, and
    `col_rsubmx`.
  + new lemma `mul_rVP`.
  + new inductions lemmas: `row_ind`, `col_ind`, `mx_ind`, `sqmx_ind`,
    `ringmx_ind`, `trigmx_ind`, `trigsqmx_ind`, `diagmx_ind`,
    `diagsqmx_ind`.
  + added missing lemma `trmx_eq0`, `det_mx11`.
  + new lemmas about diagonal and triangular matrices: `mx11_is_diag`,
    `mx11_is_trig`, `diag_mx_row`, `is_diag_mxEtrig`, `is_diag_trmx`,
    `ursubmx_trig`, `dlsubmx_diag`, `ulsubmx_trig`, `drsubmx_trig`,
    `ulsubmx_diag`, `drsubmx_diag`, `is_trig_block_mx`,
    `is_diag_block_mx`, and `det_trig`.
  + new definition `mxsub`, `rowsub` and `colsub`,
    corresponding to arbitrary submatrices/reindexation of a matrix.
    * we provide the theorems `x?(row|col)(_perm|')?Esub`, `t?permEsub`
      `[lrud]submxEsub`, `(ul|ur|dl|dr)submxEsub` for compatibility with
      ad-hoc submatrices/permutations.
    * we provide a new, configurable, induction lemma `mxsub_ind`.
    * we provide the basic theory `mxsub_id`, `eq_mxsub`, `eq_rowsub`,
      `eq_colsub`, `mxsub_eq_id`, `mxsub_eq_colsub`, `mxsub_eq_rowsub`,
      `mxsub_ffunl`, `mxsub_ffunr`, `mxsub_ffun`, `mxsub_const`,
      `mxsub_comp`, `rowsub_comp`, `colsub_comp`, `mxsubrc`, `mxsubcr`,
      `trmx_mxsub`, `row_mxsub`, `col_mxsub`, `row_rowsub`,
      `col_colsub`, and `map_mxsub`, `pid_mxErow` and `pid_mxEcol`.
    * interaction with `castmx` through lemmas `rowsub_cast`,
      `colsub_cast`, `mxsub_cast`, and `castmxEsub`.
    * `(mx|row|col)sub` are canonically additive and linear.
    * interaction with `mulmx` through lemmas `mxsub_mul`,
      `mul_rowsub_mx`, `mulmx_colsub`, and `rowsubE`.
  + added `comm_mx` and `comm_mxb` the propositional and
    boolean versions of matrix commutation, `comm_mx A B` is
    definitionally equal to `GRing.comm A B` when `A B : 'M_n.+1`, this
    is witnessed by the lemma `comm_mxE`.  New notation `all_comm_mx`
    stands for `allrel comm_mxb`. New lemmas `comm_mx_sym`,
    `comm_mx_refl`, `comm_mx0`, `comm0mx`, `comm_mx1`, `comm1mx`,
    `comm_mxN`, `comm_mxN1`, `comm_mxD`, `comm_mxB`, `comm_mx_sum`,
    `comm_mxP`, `all_comm_mxP`, `all_comm_mx1`, `all_comm_mx2P`,
    `all_comm_mx_cons`, `comm_mx_scalar`, and `comm_scalar_mx`. The
    common arguments of these lemmas `R` and `n` are maximal implicits.

- in `mxalgebra.v`,
  + completed the theory of `pinvmx` in corner cases, using lemmas
    `mulmxVp`, `mulmxKp`, `pinvmxE`, `mulVpmx`, `pinvmx_free`, and
    `pinvmx_full`.
  + new lemmas `row_base0`, `sub_kermx`, `kermx0` and `mulmx_free_eq0`.
  + new lemma `sub_sums_genmxP` (generalizes `sub_sumsmxP`).
  + new lemma `rowsub_sub`, `eq_row_full`,
    `row_full_castmx`, `row_free_castmx`, `rowsub_comp_sub`,
    `submx_rowsub`, `eqmx_rowsub_comp_perm`, `eqmx_rowsub_comp`,
    `eqmx_rowsub`, `row_freePn`, and `negb_row_free`.
  + new lemma `row_free_injr` which duplicates `row_free_inj` but
    exposing `mulmxr` for compositionality purposes (e.g. with
    `raddf_eq0`), and lemma `inj_row_free` characterizing `row_free`
    matrices `A` through `v *m A = 0 -> v = 0` for all `v`.
  + new notation `stablemx V f` asserting that `f`
    stabilizes `V`, with new theorems: `eigenvectorP`, `eqmx_stable`,
    `stablemx_row_base`, `stablemx_full`, `stablemxM`, `stablemxD`,
    `stablemxN`, `stablemxC`, `stablemx0`, `stableDmx`, `stableNmx`,
    `stable0mx`, `stableCmx`, `stablemx_sums`, and `stablemx_unit`.
  + added `comm_mx_stable`, `comm_mx_stable_ker`, and
    `comm_mx_stable_eigenspace`.
  + new definitions `maxrankfun`, `fullrankfun` which
    are "subset function" to be plugged in `rowsub`, with lemmas:
    `maxrowsub_free`, `eq_maxrowsub`, `maxrankfun_inj`,
    `maxrowsub_full`, `fullrowsub_full`, `fullrowsub_unit`,
    `fullrowsub_free`, `mxrank_fullrowsub`, `eq_fullrowsub`, and
    `fullrankfun_inj`.

- in `mxpoly.v`,
  + new lemmas `mxminpoly_minP` and `dvd_mxminpoly`.
  + new lemmas `horner_mx_diag` and `char_poly_trig`,
   `root_mxminpoly`, and `mxminpoly_diag`
  + new definitions `kermxpoly g p` (the kernel of polynomial $p(g)$).
    * new elementary theorems: `kermxpolyC`, `kermxpoly1`,
      `kermxpolyX`, `kermxpoly_min`
    * kernel lemmas: `mxdirect_kermxpoly`, `kermxpolyM`,
      `kermxpoly_prod`, and `mxdirect_sum_kermx`
    * correspondance between `eigenspace` and `kermxpoly`: `eigenspace_poly`
  + generalized eigenspace `geigenspace` and a generalization of eigenvalues
    called `eigenpoly g` (i.e. polynomials such that `kermxpoly g p`
    is nonzero, e.g. eigen polynomials of degree 1 are of the form
    `'X - a%:P` where `a` are eigenvalues), and
    * correspondance with `kermx`: `geigenspaceE`,
    * application of kernel lemmas `mxdirect_sum_geigenspace`,
    * new lemmas: `eigenpolyP`, `eigenvalue_poly`, `eigenspace_sub_geigen`,
  + new `map_mx` lemmas: `map_kermxpoly`, `map_geigenspace`, `eigenpoly_map`.
  + new lemma `horner_mx_stable`.
  + added `comm_mx_horner`, `comm_horner_mx`, `comm_horner_mx2`,
    `horner_mx_stable`, `comm_mx_stable_kermxpoly`, and
    `comm_mx_stable_geigenspace`.

- in `ssrnum.v`,
  + new lemma `ler_sum_nat`
  + new lemmas `big_real`, `sum_real`, `prod_real`, `max_real`,
    `min_real`, `bigmax_real`, and `bigmin_real`.
  + new lemma `real_lteif_distl`.

- in `interval.v`,
  + intervals and their bounds of `T` now have canonical ordered type instances
    whose ordering relations are the subset relation and the left to right
    ordering respectively. They form partially ordered types if `T` is a
    `porderType`. If `T` is a `latticeType`, they also form `tbLatticeType`
    where the join and meet are intersection and convex hull respectively. If
    `T` is an `orderType`, they are distributive, and the interval bounds are
    totally ordered. (cf Changed section)
  + new lemmas `bound_ltxx`, `subitvE`, `in_itv`, `itv_ge`, `in_itvI`,
    `itv_total_meet3E`, and `itv_total_join3E`.

### Changed

- in `ssrbool.v`, use `Reserved Notation` for `[rel _ _ : _ | _]` to
  avoid warnings with coq-8.12

- in `seq.v`, `mask` will only expand if both arguments are
  constructors, the case `mask [::] s` can be dealt with using
  `mask0s` or explicit conversion.

- in `path.v`,
  + generalized lemmas `sub_path_in`, `sub_sorted_in`, and
    `eq_path_in` for non-`eqType`s.
  + generalized lemmas `sorted_ltn_nth` and `sorted_leq_nth`
    (formerly `sorted_lt_nth` and `sorted_le_nth`, cf Renamed section) for
    non-`eqType`s.

- in `fintype.v`,
  + added lemma `ord1`, it is the same as `zmodp.ord1`,
    except `fintype.ord1` does not rely on `'I_n` zmodType structure.
  + rename `disjoint_trans` to `disjointWl`
  + lemmas `inj_card_onto` and `inj_card_bij` take a
    weaker hypothesis (i.e. `#|T| >= #|T'|` instead of `#|T| = #|T'|`
    thanks to `leq_card` under injectivity assumption).

- in `finset.v`, fixed printing of notation `[set E | x in A , y in B & P ]`

- in `bigop.v`, lemma `big_rmcond` is deprecated and has been renamed
  `big_rmcomd_in` (and aliased `big_uncond_in`, see Added). The
  variant which does not require an `eqType` is currently named
  `big_uncond` (cf Added) but it will be renamed `big_mkcond` in the
  next release.

- in `ssrAC.v`, fix `non-reversible-notation` warnings

- in `order.v`,
  + in the definition of structures, displays are removed from
    parameters of mixins and fields of classes internally and now only
    appear in parameters of structures. Consequently, each mixin is
    now parameterized by a class rather than a structure, and the
    corresponding factory parameterized by a structure is provided to
    replace the use of the mixin. These factories have the same names
    as in the mixins before this change except that `bLatticeMixin`
    and `tbLatticeMixin` have been renamed to `bottomMixin` and
    `topMixin` respectively.
  + the `dual_*` notations such as `dual_le` are now
    qualified with the `Order` module.
  + `\join^d_` and `\meet^d_` notations are now properly
    specialized for `dual_display`.
  + rephrased `comparable_(min|max)[rl]` in terms of
    `{in _, forall x y, _}`, hence reordering the arguments. Made them
    hints for smoother combination with `comparable_big[lr]`.
  + `>=< y` now stands for `[pred x | x >=< y]`
  + `>< y`  now stands for `[pred x | x >< y]`
  + and the same holds for the dual `>=<^d`, `><^d`, the product
    `>=<^p`, `><^p`, and lexicographic `>=<^l`, `><^l`.
    The previous meanings can be obtained through `>=<%O x` and `><%O x`.
  + generalized `sort_le_id` for any `porderType`.
  + the names of lemmas `join_idPl` and `join_idPr` are transposed
    to follow the naming convention.

- In `ssrnum.v`,
  + `>=< y` now stands for `[pred x | x >=< y]`
  + fixed notations `@minr` and `@maxr` to point `Order.min` and
    `Order.max` respectively.

- in `ssrint.v`, generalized `mulpz` for any `ringType`.

- in `interval.v`:
  + `x <= y ?< if c` (`lersif`) has been generalized to `porderType`, relocated
    to `order.v`, and replaced with `x < y ?<= if c'` (`lteif`) where `c'` is
    negation of `c`.
  + Many definitions and lemmas on intervals such as the membership test are
    generalized from numeric domains to ordered types.
  + Interval bounds `itv_bound : Type -> Type` are redefined with two constructors
    `BSide : bool -> T -> itv_bound T` and `BInfty : bool -> itv_bound T`.
    New notations `BLeft` and `BRight` are aliases for `BSide true` and `BSide false` respectively.
    `BInfty false` and `BInfty true` respectively means positive and negative infinity.
    `BLeft x` and `BRight x` respectively mean close and open bounds as left bounds,
    and they respectively mean open and close bounds as right bounds.
    This change gives us the canonical "left to right" ordering of interval bounds.
  + Lemmas `mid_in_itv(|oo|cc)` have been generalized from
    `realFieldType` to `numFieldType`.

- In `matrix.v`, generalized `diag_mx_comm` and `scalar_mx_comm` to
  all `n`, instead of `n'.+1`, thanks to `commmmx`.

### Renamed

- in `ssrnat.v`
  + `iter_add` -> `iterD`
  + `maxn_mul(l|r)` -> `maxnM(l|r)`
  + `minn_mul(l|r)` -> `minnM(l|r)`
  + `odd_(opp|mul|exp)` -> `odd(N|M|X)`
  + `sqrn_sub` -> `sqrnB`

- in `div.v`
  + `coprime_mul(l|r)` -> `coprimeM(l|r)`
  + `coprime_exp(l|r)` -> `coprimeX(l|r)`

- in `prime.v`
  + `primes_(mul|exp)` -> `primes(M|X)`
  + `pnat_(mul|exp)` -> `pnat(M|X)`

- in `seq.v`,
  + `iota_add(|l)` -> `iotaD(|l)`
  + `allpairs_(cons|cat)r` -> `mem_allpairs_(cons|cat)r`
    (`allpairs_consr` and `allpairs_catr` are now deprecated alias,
    and will be attributed to the new `perm_allpairs_catr`).

- in `path.v`,
  + `eq_sorted(_irr)` -> `(irr_)sorted_eq`
  + `sorted_(lt|le)_nth` -> `sorted_(ltn|leq)_nth`
  + `(ltn|leq)_index` -> `sorted_(ltn|leq)_index`
  + `subseq_order_path` -> `subseq_path`

- in `fintype.v`
  + `bump_addl` -> `bumpDl`
  + `unbump_addl` -> `unbumpDl`

- in `finset.v`,
  + `mem_imset` -> `imset_f` (with deprecation alias, cf. Added section)
  + `mem_imset2` -> `imset2_f` (with deprecation alias, cf. Added section)

- in `bigop.v`
  + `big_rmcond` -> `big_rmcond_in` (cf Changed section)
  + `mulm_add(l|r)` -> `mulmD(l|r)`

- in `order.v`, `eq_sorted_(le|lt)` -> `(le|lt)_sorted_eq`

- in `interval.v`, we deprecate, rename, and relocate to `order.v` the following:
  + `lersif_(trans|anti)` -> `lteif_(trans|anti)`
  + `lersif(xx|NF|S|T|F|W)` -> `lteif(xx|NF|S|T|F|W)`
  + `lersif_(andb|orb|imply)` -> `lteif_(andb|orb|imply)`
  + `ltrW_lersif` -> `ltrW_lteif`
  + `lersifN` -> `lteifNE`
  + `lersif_(min|max)(l|r)` -> ` lteif_(min|max)(l|r)`

- in `interval.v`, we deprecate, rename, and relocate to `ssrnum.v` the following:
  + `subr_lersif(r0|0r|0)` -> `subr_lteif(r0|0r|0)`
  + `lersif01` -> `lteif01`
  + `lersif_(oppl|oppr|0oppr|oppr0|opp2|oppE)` -> `lteif_(oppl|oppr|0oppr|oppr0|opp2|oppE)`
  + `lersif_add2(|l|r)` -> `lteif_add2(|l|r)`
  + `lersif_sub(l|r)_add(l|r)` -> `lteif_sub(l|r)_add(l|r)`
  + `lersif_sub_add(l|r)` -> `lteif_sub_add(l|r)`
  + `lersif_(p|n)mul2(l|r)` -> `lteif_(p|n)mul2(l|r)`
  + `real_lersifN` -> `real_lteifNE`
  + `real_lersif_norm(l|r)` -> `real_lteif_norm(l|r)`
  + `lersif_nnormr` -> `lteif_nnormr`
  + `lersif_norm(l|r)` -> `lteif_norm(l|r)`
  + `lersif_distl` -> `lteif_distl`
  + `lersif_(p|n)div(l|r)_mul(l|r)` -> `lteif_(p|n)div(l|r)_mul(l|r)`

- in `interval.v`, we deprecate and replace the following:
  + `lersif_in_itv` -> `lteif_in_itv`
  + `itv_gte` -> `itv_ge`
  + `l(t|e)r_in_itv` -> `lt_in_itv`

- in `ssralg.v`, `prodrMn`-> `prodrMn_const` (with deprecation alias,
  cf. Added section)

- in `ssrint.v`, `polyC_mulrz` -> `polyCMz`

- in `poly.v`
  + `polyC_(add|opp|sub|muln|mul|inv)` -> `polyC(D|N|B|Mn|M|V)`
  + `lead_coef_opp` -> `lead_coefN`
  + `derivn_sub` -> `derivnB`

- in `polydiv.v`
  + `rdivp_add(l|r)` -> `rdivpD(l|r)`
  + `rmodp_add` -> `rmodpD`
  + `dvdp_scale(l|r)` -> `dvdpZ(l|r)`
  + `dvdp_opp` -> `dvdpNl`
  + `coprimep_scale(l|r)` -> `coprimepZ(l|r)`
  + `coprimep_mul(l|r)` -> `coprimepM(l|r)`
  + `modp_scale(l|r)` -> `modpZ(l|r)`
  + `modp_(opp|add|scalel|scaler)` -> `modp(N|D|Zl|Zr)`
  + `divp_(opp|add|scalel|scaler)` -> `divp(N|D|Zl|Zr)`

- in `matrix.v`, `map_mx_sub` -> `map_mxB`

- in `mxalgebra.v`, `mulsmx_add(l|r)` -> `mulsmxD(l|r)`

- in `vector.v`, `limg_add` -> `limgD`

- in `intdiv.v`
  + `coprimez_mul(l|r)` -> `coprimezM(l|r)`
  + `coprimez_exp(l|r)` -> `coprimezX(l|r)`

### Removed

- in `ssrnat.v`, we remove the compatibility module `mc_1_9`.

- in `interval.v`, we remove the following:
  + `le_bound(l|r)` (use `Order.le` instead)
  + `le_bound(l|r)_refl` (use `lexx` instead)
  + `le_bound(l|r)_anti` (use `eq_le` instead)
  + `le_bound(l|r)_trans` (use `le_trans` instead)
  + `le_bound(l|r)_bb` (use `bound_lexx` instead)
  + `le_bound(l|r)_total` (use `le_total` instead)

- in `interval.v`, we deprecate the following:
  + `itv_intersection` (use `Order.meet` instead)
  + `itv_intersection1i` (use `meet1x` instead)
  + `itv_intersectioni1` (use `meetx1` instead)
  + `itv_intersectionii` (use `meetxx` instead)
  + `itv_intersectionC` (use `meetC` instead)
  + `itv_intersectionA` (use `meetA` instead)

- in `mxpoly.v`, we deprecate `scalar_mx_comm`, and advise to use
  `comm_mxC` instead (with maximal implicit arguments `R` and `n`).

### Infrastructure

- in all the hierarchies (in `eqtype.v`, `choice.v`, `order.v`,
  `ssralg.v`,...), the `class_of` records of structures are turned
  into primitive records to prevent prevent potential issues of
  ambiguous paths and convertibility of structure instances.

- across the library, the following constants have been tuned to only
  reduce when they do not expose a match: `subn_rec`, `decode_rec`,
  `nth` (thus avoiding a notorious problem of ``p`_0`` expanding too
  eagerly), `set_nth`, `take`, `drop`, `eqseq`, `incr_nth`, `elogn2`,
  `binomial_rec`, `sumpT`.

## [1.11.0] - 2020-06-09

This release is compatible with Coq versions 8.7, 8.8, 8.9, 8.10, and 8.11.

- Added lemmas about monotony of functions `nat -> T` where `T` is an
  ordered type: `homo_ltn_lt_in`, `incn_inP`, `nondecn_inP`,
  `nhomo_ltn_lt_in`, `decn_inP`, `nonincn_inP`, `homo_ltn_lt`,
  `incnP`, `nondecnP`, `nhomo_ltn_lt`, `decnP`, `nonincnP` in file
  `order.v`.

- Added lemmas for swaping arguments of homomorphisms and
  monomorphisms: `homo_sym`, `mono_sym`, `homo_sym_in`, `mono_sym_in`,
  `homo_sym_in11`, `mono_sym_in11` in `ssrbool.v`

### Added

- in `ssrnum.v`, new lemmas:
  + `(real_)ltr_normlW`, `(real_)ltrNnormlW`, `(real_)ler_normlW`, `(real_)lerNnormlW`
  + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distlC_addr`, `(real_)ler_distlC_addr`,
    `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distlC_subl`, `(real_)ler_distlC_subl`

- in `order.v`, defining `min` and `max` independently from `meet` and
  `join`, and providing a theory about for min and max, hence generalizing
  the theory of `Num.min` and `Num.max` from versions <= `1.10`, instead
  of specializing to total order as in `1.11+beta1`:
  ```
  Definition min (T : porderType) (x y : T) := if x < y then x else y.
  Definition max (T : porderType) (x y : T) := if x < y then y else x.
  ```
  + Lemmas: `min_l`, `min_r`, `max_l`, `max_r`, `minxx`, `maxxx`, `eq_minl`, `eq_maxr`,
    `min_idPl`, `max_idPr`, `min_minxK`, `min_minKx`, `max_maxxK`, `max_maxKx`,
    `comparable_minl`, `comparable_minr`,  `comparable_maxl`, and `comparable_maxr`
  + Lemmas about interaction with lattice operations:  `meetEtotal`, `joinEtotal`,
  + Lemmas under condition of pairwise comparability of a (sub)set of their arguments:
    `comparable_minC`, `comparable_maxC`, `comparable_eq_minr`, `comparable_eq_maxl`,
    `comparable_le_minr`, `comparable_le_minl`, `comparable_min_idPr`,
    `comparable_max_idPl`, `comparableP`, `comparable_lt_minr`,
    `comparable_lt_minl`, `comparable_le_maxr`, `comparable_le_maxl`,
    `comparable_lt_maxr`, `comparable_lt_maxl`, `comparable_minxK`, `comparable_minKx`,
    `comparable_maxxK`, `comparable_maxKx`,
    `comparable_minA`, `comparable_maxA`, `comparable_max_minl`, `comparable_min_maxl`,
    `comparable_minAC`, `comparable_maxAC`, `comparable_minCA`, `comparable_maxCA`,
    `comparable_minACA`, `comparable_maxACA`, `comparable_max_minr`, `comparable_min_maxr`
  + and the same but in a total order: `minC`, `maxC`, `minA`, `maxA`, `minAC`, `maxAC`,
    `minCA`, `maxCA`, `minACA`, `maxACA`, `eq_minr`, `eq_maxl`,
    `min_idPr`, `max_idPl`, `le_minr`, `le_minl`, `lt_minr`,
    `lt_minl`, `le_maxr`,`le_maxl`, `lt_maxr`, `lt_maxl`, `minxK`, `minKx`,
    `maxxK`, `maxKx`, `max_minl`, `min_maxl`, `max_minr`, `min_maxr`
- in `ssrnum.v`, theory about `min` and `max` extended to `numDomainType`:
  + Lemmas: `real_oppr_max`, `real_oppr_min`, `real_addr_minl`, `real_addr_minr`,
    `real_addr_maxl`, `real_addr_maxr`, `minr_pmulr`, `maxr_pmulr`, `real_maxr_nmulr`,
    `real_minr_nmulr`, `minr_pmull`, `maxr_pmull`, `real_minr_nmull`, `real_maxr_nmull`,
    `real_maxrN`, `real_maxNr`, `real_minrN`, `real_minNr`
- the compatibility module `ssrnum.mc_1_10` was extended to  support definitional
  compatibility with `min` and `max` which had been lost in `1.11+beta1` for most instances.
- in `fintype.v`, new lemmas: `seq_sub_default`, `seq_subE`
- in `order.v`, new "unfolding" lemmas: `minEnat` and `maxEnat`

- in `ssrbool.v`
  + lemmas about the `cancel` predicate and `{in _, _}`/`{on _, _}` notations:
    * `onW_can`, `onW_can_in`, `in_onW_can`, `onS_can`, `onS_can_in`, `in_onS_can`
  + lemmas about the `cancel` predicate and injective functions:
    * `inj_can_sym_in_on`, `inj_can_sym_on`, `inj_can_sym_in`

### Changed

- in `order.v`, `le_xor_gt`, `lt_xor_ge`, `compare`, `incompare`, `lel_xor_gt`,
  `ltl_xor_ge`, `comparel`, `incomparel` have more parameters, so that the
  the following now deal with `min` and `max`
  + `comparable_ltgtP`, `comparable_leP`, `comparable_ltP`, `comparableP`
  + `lcomparableP`, `lcomparable_ltgtP`, `lcomparable_leP`, `lcomparable_ltP`, `ltgtP`
- in `order.v`:
  + `[arg min_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
  + `[arg max_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
  + added `comparable_arg_minP`,  `comparable_arg_maxP`,  `real_arg_minP`,  `real_arg_maxP`,
    in order to take advantage of the former generalizations.
- in `ssrnum.v`, `maxr` is a notation for `(@Order.max ring_display _)` (was `Order.join`)
  (resp. `minr` is a notation for `(@Order.min ring_display _)`)
- in `ssrnum.v`, `ler_xor_gt`, `ltr_xor_ge`, `comparer`,
  `ger0_xor_lt0`, `ler0_xor_gt0`, `comparer0` have now more parameters, so that
  the following now deal with min and max:
  + `real_leP`, `real_ltP x y`, `real_ltgtP`, `real_ge0P`, `real_le0P`, `real_ltgt0P`
  + `lerP`, `ltrP`, `ltrgtP`, `ger0P`, `ler0P`, `ltrgt0P`
- in `ssrnum.v`, the following have been restated (which were formerly derived from
  `order.v` and stated with specializations of the `meet` and `join` operators):
   + `minrC`, `minrr`, `minr_l`, `minr_r`, `maxrC`, `maxrr`, `maxr_l`,
     `maxr_r`, `minrA`, `minrCA`, `minrAC`, `maxrA`, `maxrCA`, `maxrAC`
   + `eqr_minl`, `eqr_minr`, `eqr_maxl`, `eqr_maxr`, `ler_minr`, `ler_minl`,
     `ler_maxr`, `ler_maxl`, `ltr_minr`, `ltr_minl`, `ltr_maxr`, `ltr_maxl`
   + `minrK`, `minKr`, `maxr_minl`, `maxr_minr`, `minr_maxl`, `minr_maxr`
- The new definitions of `min` and `max` may require the following rewrite rules
  changes when dealing with `max` and `min` instead of `meet` and `join`:
  + `ltexI` -> `(le_minr,lt_minr)`
  + `lteIx` -> `(le_minl,lt_minl)`
  + `ltexU` -> `(le_maxr,lt_maxr)`
  + `lteUx` -> `(le_maxl,lt_maxl)`
  + `lexU` -> `le_maxr`
  + `ltxU` -> `lt_maxr`
  + `lexU` -> `le_maxr`

- in `ssrbool.v`
  + lemmas about monotone functions and the `{in _, _}` notation:
    * `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, `monoRL_in`, `can_mono_in`

### Renamed

- in `fintype` we deprecate and rename the following:
  + `arg_minP` -> `arg_minnP`
  + `arg_maxP` -> `arg_maxnP`

- in `order.v`, in module `NatOrder`, renamings:
  + `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`,
    `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`

### Removed

- in `order.v`, removed `total_display` (was used to provide the notation
  `max` for `join` and `min` for `meet`).
- in `order.v`, removed `minnE` and `maxnE`
- in `order.v`,
  + removed `meetEnat` (in favor of `meetEtotal` followed by `minEnat`)
  + removed `joinEnat` (in favor of `joinEtotal` followed by `maxEnat`)

## [1.11+beta1] - 2020-04-15

This release is compatible with Coq versions 8.7, 8.8, 8.9 and 8.10.

### Added

- Arithmetic theorems in ssrnat, div and prime about `logn`,
    `coprime`, `gcd`, `lcm` and `partn`: `logn_coprime`, `logn_gcd`,
    `logn_lcm`, `eq_partn_from_log` and `eqn_from_log`.

- Lemmas `ltnNleqif`, `eq_leqif`, `eqTleqif` in `ssrnat`

- Lemmas `eqEtupe`, `tnthS` and `tnth_nseq` in `tuple`

- Ported `order.v` from the finmap library, which provides structures of ordered
  sets (`porderType`, `latticeType`, `distrLatticeType`, `orderType`, etc.) and
  its theory.

- Lemmas `path_map`, `eq_path_in`, `sub_path_in`, `path_sortedE`,
  `sub_sorted` and `sub_sorted_in` in `path` (and refactored related proofs)

- Added lemmas `hasNfind`, `memNindex` and `findP` in `seq`

- Added lemmas `foldr_rcons`, `foldl_rcons`, `scanl_rcons` and
  `nth_cons_scanl` in `seq`

- ssrAC tactics, see header of `ssreflect/ssrAC.v` for documentation
  of `(AC patternshape reordering)`, `(ACl reordering)` `(ACof
  reordering reordering)`, `op.[AC patternshape reordering]`, `op.[ACl
  reordering]` and `op.[ACof reordering reordering]`.

- Added definition `cast_perm` with a group morphism canonical
  structure, and lemmas `permX_fix`, `imset_perm1`, `permS0`,
  `permS1`, `cast_perm_id`, `cast_ord_permE`, `cast_permE`,
  `cast_perm_comp`, `cast_permK`, `cast_permKV`, `cast_perm_inj`,
  `cast_perm_sym`,`cast_perm_morphM`, and `isom_cast_perm` in `perm`
  and `restr_perm_commute` in `action`.

- Added `card_porbit_neq0`, `porbitP`, and `porbitPmin` in `perm`

- Added definition `Sym` with a group set canonical structure and
  lemmas `card_Sn` and `card_Sym` in `perm` and `SymE` in `action`

### Changed

- Reorganized the algebraic hierarchy and the theory of `ssrnum.v`.
  + `numDomainType` and `realDomainType` get inheritances respectively from
    `porderType` and `orderType`.
  + `normedZmodType` is a new structure for `numDomainType` indexed normed
    additive abelian groups.
  + `[arg minr_( i < n | P ) F]` and `[arg maxr_( i < n | P ) F]` notations are
    removed. Now `[arg min_( i < n | P ) F]` and `[arg max_( i < n | P ) F]`
    notations are defined in `nat_scope` (specialized for `nat`), `order_scope`
    (general one), and `ring_scope` (specialized for `ring_display`). Lemma
    `fintype.arg_minP` is aliased to `arg_minnP` and the same for `arg_maxnP`.
  + The following lemmas are generalized, renamed, and relocated to `order.v`:
    * `ltr_def` -> `lt_def`
    * `(ger|gtr)E` -> `(ge|gt)E`
    * `(le|lt|lte)rr` -> `(le|lt|lte)xx`
    * `ltrW` -> `ltW`
    * `ltr_neqAle` -> `lt_neqAle`
    * `ler_eqVlt` -> `le_eqVlt`
    * `(gtr|ltr)_eqF` -> `(gt|lt)_eqF`
    * `ler_anti`, `ler_asym` -> `le_anti`
    * `eqr_le` -> `eq_le`
    * `(ltr|ler_lt|ltr_le|ler)_trans` -> `(lt|le_lt|lt_le|le)_trans`
    * `lerifP` -> `leifP`
    * `(ltr|ltr_le|ler_lt)_asym` -> `(lt|lt_le|le_lt)_asym`
    * `lter_anti` -> `lte_anti`
    * `ltr_geF` -> `lt_geF`
    * `ler_gtF` -> `le_gtF`
    * `ltr_gtF` -> `lt_gtF`
    * `lt(r|nr|rn)W_(n)homo(_in)` -> `ltW_(n)homo(_in)`
    * `inj_(n)homo_lt(r|nr|rn)(_in)` -> `inj_(n)homo_lt(_in)`
    * `(inc|dec)(r|nr|rn)_inj(_in)` -> `(inc_dec)_inj(_in)`
    * `le(r|nr|rn)W_(n)mono(_in)` -> `leW_(n)mono(_in)`
    * `lenr_(n)mono(_in)` -> `le_(n)mono(_in)`
    * `lerif_(refl|trans|le|eq)` -> `leif_(refl|trans|le|eq)`
    * `(ger|ltr)_lerif` -> `(ge|lt)_leif`
    * `(n)mono(_in)_lerif` -> `(n)mono(_in)_leif`
    * `(ler|ltr)_total` -> `(le|lt)_total`
    * `wlog_(ler|ltr)` -> `wlog_(le|lt)`
    * `ltrNge` -> `ltNge`
    * `lerNgt` -> `leNgt`
    * `neqr_lt` -> `neq_lt`
    * `eqr_(le|lt)(LR|RL)` -> `eq_(le|lt)(LR|RL)`
    * `eqr_(min|max)(l|r)` -> `eq_(meet|join)(l|r)`
    * `ler_minr` -> `lexI`
    * `ler_minl` -> `leIx`
    * `ler_maxr` -> `lexU`
    * `ler_maxl` -> `leUx`
    * `lt(e)r_min(r|l)` -> `lt(e)(xI|Ix)`
    * `lt(e)r_max(r|l)` -> `lt(e)(xU|Ux)`
    * `minrK` -> `meetUKC`
    * `minKr` -> `joinKIC`
    * `maxr_min(l|r)` -> `joinI(l|r)`
    * `minr_max(l|r)` -> `meetU(l|r)`
    * `minrP`, `maxrP` -> `leP`, `ltP`

      Replacing `minrP` and `maxrP` with `leP` and `ltP` may require to provide some arguments explicitly.
      The former ones respectively try to match with `minr` and `maxr` first but the latter ones try that in the order of `<`, `<=`, `maxr`, and `minr`.
    * `(minr|maxr)(r|C|A|CA|AC)` -> `(meet|join)(xx|C|A|CA|AC)`
    * `minr_(l|r)` -> `meet_(l|r)`
    * `maxr_(l|r)` -> `join_(l|r)`
    * `arg_minrP` -> `arg_minP`
    * `arg_maxrP` -> `arg_maxP`
  + Generalized the following lemmas as properties of `normedDomainType`:
    `normr0`, `normr0P`, `normr_eq0`, `distrC`, `normr_id`, `normr_ge0`,
    `normr_le0`, `normr_lt0`, `normr_gt0`, `normrE`, `normr_real`,
    `ler_norm_sum`, `ler_norm_sub`, `ler_dist_add`, `ler_sub_norm_add`,
    `ler_sub_dist`, `ler_dist_dist`, `ler_dist_norm_add`, `ler_nnorml`,
    `ltr_nnorml`, `lter_nnormr`.
  + The compatibility layer for the version 1.10 is provided as the
    `ssrnum.mc_1_10` module. One may compile proofs compatible with the version
    1.10 in newer versions by using the `mc_1_10.Num` module instead of the
    `Num` module. However, instances of the number structures may require
    changes.

- Extended comparison predicates `leqP`, `ltnP`, and `ltngtP` in ssrnat to
  allow case analysis on `minn` and `maxn`.
  + The compatibility layer for the version 1.10 is provided as the
    `ssrnat.mc_1_10` module. One may compile proofs compatible with the version
    1.10 in newer versions by using this module.

- The definition of `all2` was slightly altered for a better interaction with
  the guard condition (#469)

### Renamed

- `real_lerP` -> `real_leP`
- `real_ltrP` -> `real_ltP`
- `real_ltrNge` -> `real_ltNge`
- `real_lerNgt` -> `real_leNgt`
- `real_ltrgtP` -> `real_ltgtP`
- `real_ger0P` -> `real_ge0P`
- `real_ltrgt0P` -> `real_ltgt0P`
- `lerif_nat` -> `leif_nat_r`
- Replaced `lerif` with `leif` in the following names of lemmas:
  + `lerif_subLR`, `lerif_subRL`, `lerif_add`, `lerif_sum`, `lerif_0_sum`,
    `real_lerif_norm`, `lerif_pmul`, `lerif_nmul`, `lerif_pprod`,
    `real_lerif_mean_square_scaled`, `real_lerif_AGM2_scaled`,
    `lerif_AGM_scaled`, `real_lerif_mean_square`, `real_lerif_AGM2`,
    `lerif_AGM`, `relif_mean_square_scaled`, `lerif_AGM2_scaled`,
    `lerif_mean_square`, `lerif_AGM2`, `lerif_normC_Re_Creal`, `lerif_Re_Creal`,
    `lerif_rootC_AGM`.
- The following naming inconsistencies have been fixed in `ssrnat.v`:
  + `homo_inj_lt(_in)` -> `inj_homo_ltn(_in)`
  + `(inc|dec)r_inj(_in)` -> `(inc|dec)n_inj(_in)`
- switching long suffixes to short suffixes
  + `odd_add` -> `oddD`
  + `odd_sub` -> `oddB`
  + `take_addn` -> `takeD`
  + `rot_addn` -> `rotD`
  + `nseq_addn` -> `nseqD`
- Replaced `cycle` by `orbit` in `perm/action`:
  + `pcycle` -> `porbit`
  + `pcycles` -> `porbits`
  + `pcycleE` -> `porbitE`
  + `pcycle_actperm` -> `porbit_actperm`
  + `mem_pcycle` -> `mem_porbit`
  + `pcycle_id` -> `porbit_id`
  + `uniq_traject_pcycle` -> `uniq_traject_porbit`
  + `pcycle_traject` -> `porbit_traject`
  + `iter_pcycle` -> `iter_porbit`
  + `eq_pcycle_mem` -> `eq_porbit_mem`
  + `pcycle_sym` -> `porbit_sym`
  + `pcycle_perm` -> `porbit_perm`
  + `ncycles_mul_tperm` -> `porbits_mul_tperm`

### Removed

The following were deprecated since release 1.9.0
- `tuple_perm_eqP` (use `tuple_permP` instead, from `perm.v`)
- `eq_big_perm` (use `perm_big` instead, from `bigop.v`)
- `perm_eqP` (use `permP` instead, from seq.v)
- `perm_eqlP` (use `permPl` instead)
- `perm_eqrP` (use `permPr` instead)
- `perm_eqlE` (use `permEl` instead)
- `perm_eq_refl` (use `perm_refl` instead)
- `perm_eq_sym` (use `perm_sym` instead)
- `perm_eq_trans` (use `perm_trans` instead)
- `perm_eq_size` (use `perm_size` instead)
- `perm_eq_mem` (use `perm_mem` instead)
- `perm_eq_uniq` (use `perm_uniq` instead)

## [1.10.0] - 2019-11-29

This release is compatible with Coq versions 8.9 and 8.10.

### Added

- Added a `void` notation for the `Empty_set` type of the standard library, the
  canonical injection `of_void` and its cancellation lemma `of_voidK`, and
  `eq`, `choice`, `count` and `fin` instances.

- Added `ltn_ind` general induction principle for `nat` variables, helper lemmas `ubnP`, `ltnSE`, ubnPleq, ubnPgeq and ubnPeq, in support of a generalized induction idiom for `nat` measures that does not rely on the `{-2}` numerical occurrence selector, and purged this idiom from the `mathcomp` library (see below).

- Added fixpoint and cofixpoint constructions to `finset`: `fixset`,
  `cofixset` and `fix_order`, with a few theorems about them

- Added functions `tuple_of_finfun`, `finfun_of_tuple`, and their
  "cancellation" lemmas.

- Added theorems `totient_prime` and `Euclid_dvd_prod` in `prime.v`

- Added theorems `ffact_prod`, `prime_modn_expSn` and `fermat_little`
  in `binomial.v`

- Added theorems `flatten_map1`, `allpairs_consr`, `mask_filter`,
  `all_filter`, `all_pmap`, and `all_allpairsP` in `seq.v`.

- Added theorems `nth_rcons_default`, `undup_rcons`, `undup_cat` and
  `undup_flatten_nseq` in `seq.v`

- Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`,
  `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`,
  `existsPn`, `exists_inPn`, `forallPn`, `forall_inPn`,
  `eq_enum_rank_in`, `enum_rank_in_inj`, `lshift_inj`, and
  `rshift_inj`.

- Bigop theorems: `index_enum_uniq`, `big_rmcond`, `bigD1_seq`,
  `big_enum_val_cond`, `big_enum_rank_cond`,
  `big_enum_val`, `big_enum_rank`, `big_set`,
  `big_enumP`, `big_enum_cond`, `big_enum`

- Arithmetic theorems in ssrnat and div:
  - some trivial results in ssrnat: `ltn_predL`, `ltn_predRL`,
    `ltn_subrR`, `leq_subrR`, `ltn_subrL` and `predn_sub`,
  - theorems about `n <=/< p +/- m` and `m +/- n <=/< p`:
    `leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`, `leq_subCl`,
    `leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and
    `ltn_subCl`,
  - some commutations between modulo and division: `modn_divl` and
    `divn_modl`,
  - theorems about the euclidean division of additions and subtraction,
     + without preconditions of divisibility: `edivnD`, `edivnB`,
       `divnD`, `divnB`, `modnD`, `modnB`,
     + with divisibility of one argument: `divnDMl`, `divnMBl`,
       `divnBMl`, `divnBl` and `divnBr`,
     + specialization of the former theorems for .+1 and .-1:
       `edivnS`, `divnS`, `modnS`, `edivn_pred`, `divn_pred` and
       `modn_pred`.

- Added `sort_rec1` and `sortE` to help inductive reasoning on `sort`.

- Added map/parametricity theorems about `path`, `sort`, and `sorted`:
  `homo_path`, `mono_path`, `homo_path_in`, `mono_path_in`,
  `homo_sorted`, `mono_sorted`, `map_merge`, `merge_map`, `map_sort`,
  `sort_map`, `sorted_map`, `homo_sorted_in`, `mono_sorted_in`.

- Extracting lemma `fpathE` from `fpathP`, and shortening the proof of
  the latter.

- Added the theorem `perm_iota_sort` to express that the sorting of
  any sequence `s` is equal to a mapping of `iota 0 (size s)` to the
  nth elements of `s`, so that one can still reason on `nat`, even
  though the elements of `s` are not in an `eqType`.

- Added stability theorems about `merge` and `sort`: `sorted_merge`,
  `merge_stable_path`, `merge_stable_sorted`, `sorted_sort`, `sort_stable`,
  `filter_sort`, `mask_sort`, `sorted_mask_sort`, `subseq_sort`,
  `sorted_subseq_sort`, and `mem2_sort`.

- New algebraic interfaces in `ssralg.v`: comAlgebra and
  comUnitAlgebra for commutative and commutative-unitary algebras.

- Initial property for polynomials in algebras:
  New canonical lrMoprphism `horner_alg` evaluating a polynomial in an element
  of an algebra. The theory include the lemmas `in_alg_comm`, `horner_algC`,
  `horner_algX`, `poly_alg_initial`.

- Added lemmas on commutation with difference, big sum and prod:
  `commrB`, `commr_sum`, `commr_prod`.

- Added a few basic seq lemmas about `nseq`, `take` and `drop`:
  `nseq_addn`, `take_take`, `take_drop`, `take_addn`, `takeC`,
  `take_nseq`, `drop_nseq`, `rev_nseq`, `take_iota`, `drop_iota`.

- Added ssrfun theorem `inj_compr`.

- Added theorems `mem2E`, `nextE`, `mem_fcycle`, `inj_cycle`,
  `take_traject`, `trajectD` and `cycle_catC` in `path.v`

- Added lemmas about `cycle`, `connect`, `fconnect`, `order` and
  `orbit` in `fingraph.v`:
  - lemma `connect_cycle`,
  - lemmas `in_orbit`, `order_gt0`, `findex_eq0`, `mem_orbit`,
    `image_orbit`,
  - lemmas `fcycle_rconsE`, `fcycle_consE`, `fcycle_consEflatten` and
    `undup_cycle_cons` which operate under the precondition that the
    sequence `x :: p` is a cycle for f (i.e. `fcycle f (x :: p)`).
  - lemmas which operate under the precondition there is a sequence
    `p` which is a cycle for `f` (i.e. `fcycle f p`):
    `order_le_cycle`, `finv_cycle`, `f_finv_cycle`, `finv_f_cycle`,
    `finv_inj_cycle`, `iter_finv_cycle`, `cycle_orbit_cycle`,
    `fpath_finv_cycle`, `fpath_finv_f_cycle`, `fpath_f_finv_cycle`,
    `prevE`, `fcycleEflatten`, `fcycle_undup`, `in_orbit_cycle`,
    `eq_order_cycle`, `iter_order_cycle`,
  - lemmas `injectivePcycle`, `orbitPcycle`, `fconnect_eqVf`,
    `order_id_cycle`, `orderPcycle`, `fconnect_f`, `fconnect_findex`.

- Added lemma `rot_index` which explicits the index given by `rot_to`.

- Added tactic `tfae` to split an equivalence between n+1 propositions
  into n+1 goals, and referenced orbitPcycle as a reference of use.

### Changed

- Replaced the legacy generalised induction idiom with a more robust one
that does not rely on the `{-2}` numerical occurrence selector, using
new `ssrnat` helper lemmas `ltn_ind`, `ubnP`, `ubnPleq`,  ...., (see above). The new idiom is documented in `ssrnat`.
   This change anticipates an expected evolution of `fintype` to integrate `finmap`. It is likely that the new definition of the `#|A|` notation will hide multiple occurrences of `A`, which will break the `{-2}` induction idiom. Client libraries should update before the 1.11 release (see [PR #434](https://github.com/math-comp/math-comp/pull/434) for examples).

 - Replaced the use of the accidental convertibility between `enum A` and
   `filter A (index_enum T)` with more explicit lemmas `big_enumP`, `big_enum`, `big_enum_cond`, `big_image` added to the `bigop` library, and deprecated the `filter_index_enum` lemma that states the corresponding equality. Both convertibility and equality may no longer hold in future `mathcomp` releases when sets over `finType`s are generalised to finite sets over `choiceType`s, so client libraries should stop relying on this identity. File `bigop.v` has some boilerplate to help with the port; also see [PR #441](https://github.com/math-comp/math-comp/pull/441) for examples.

 - Restricted `big_image`, `big_image_cond`, `big_image_id` and `big_image_cond_id`
 to `bigop`s over _abelian_ monoids, anticipating the change in the definition of `enum`. This may introduce some incompatibilities - non-abelian instances should be dealt with a combination of `big_map` and `big_enumP`.

- `eqVneq` lemma is changed from `{x = y} + {x != y}` to
  `eq_xor_neq x y (y == x) (x == y)`, on which a case analysis performs
  simultaneous replacement of expressions of the form `x == y` and `y == x`
  by `true` or `false`, while keeping the ability to use it in the way
  it was used before.

- Generalized the `allpairs_catr` lemma to the case where the types of `s`,
  `t1`, and `t2` are non-`eqType`s in `[seq E | i <- s, j <- t1 ++ t2]`.

- Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.

- Generalized `sort` to non-`eqType`s (as well as `merge`,
  `merge_sort_push`, `merge_sort_pop`), together with all the lemmas
  that did not really rely on an `eqType`: `size_merge`, `size_sort`,
  `merge_path`, `merge_sorted`, `sort_sorted`, `path_min_sorted`
  (which statement was modified to remove the dependency in `eqType`),
  and `order_path_min`.

- `compare_nat` type family and `ltngtP` comparison predicate are changed
  from `compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)`
  to `compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`,
  to make it tries to match subterms with `m < n` first, `m <= n`, then
  `m == n`.
  + The compatibility layer for the version 1.9 is provided as the
    `ssrnat.mc_1_9` module. One may compile proofs compatible with the version
    1.9 in newer versions by using this module.

- Moved `iter_in` to ssrnat and reordered its arguments.

- Notation `[<-> P0 ; .. ; Pn]` now forces `Pi` to be of type `Prop`.

### Removed

- `fin_inj_bij` lemma is removed as a duplicate of `injF_bij` lemma
  from `fintype` library.

### Infrastructure

- `Makefile` now supports the `test-suite` and `only` targets. Currently,
  `make test-suite` will verify the implementation of mathematical structures
  and their inheritances of MathComp automatically, by using the `hierarchy.ml`
  utility. One can use the `only` target to build the sub-libraries of MathComp
  specified by the `TGTS` variable, e.g.,
  `make only TGTS="ssreflect/all_ssreflect.vo fingroup/all_fingroup.vo"`.

- `Makefile`now supports a `doc` target to build the documentation as made
   available on https://mathcomp.github.io/htmldoc/index.html

## [1.9.0] - 2019-05-22

MathComp 1.9.0 is compatible with Coq 8.7, 8.8, 8.9 and 8.10beta1.
Minor releases will remain compatible with Coq 8.9 and 8.10; compatibility with earlier
versions may be dropped.

### Added

- `nonPropType`, an interface for non-`Prop` types, and `{pred T}` and
   `relpre f r`, all of which will be in the Coq 8.10 core SSreflect library.

- `deprecate old_id new_id`, notation for `new_id` that prints a deprecation
  warning for `old_id`; `Import Deprecation.Silent` turns off those warnings,
  `Import Deprecation.Reject` raises errors instead of only warning.

- `filter_nseq`, `count_nseq`, `mem_nseq`,
  `rcons_inj`, `rcons_injl`, `rcons_injr`, `nthK`, `sumn_rot`.

- some `perm_eq` lemmas: `perm_cat[lr]`, `perm_nilP`,
  `perm_consP`, `perm_has`, `perm_flatten`, `perm_sumn`.

- computing (efficiently) (item, multiplicity) tallies of sequences over an
  `eqType`: `tally s`, `incr_tally bs x`, `bs \is a wf_tally`, `tally_seq bs`.

### Changed

- definition of `PredType` which now takes only a `P -> pred T` function;
  definition of `simpl_rel` to improve simplification by `inE`. Both these
  changes will be in the Coq 8.10 SSReflect core library.

- definition of `permutations s` now uses an optimal algorithm (in space _and_
  time) to generate all permutations of s back-to-front, using `tally s`.

### Renamed

- `perm_eqP` -> `permP` (`seq.permP` if `perm.v` is also imported)
- `perm_eqlP` -> `permPl`
- `perm_eqrP` -> `permPr`
- `perm_eqlE` -> `permEl`
- `perm_eq_refl` -> `perm_refl`
- `perm_eq_sym` -> `perm_sym`
- `perm_eq_trans` -> `perm_trans`
- `perm_eq_size` -> `perm_size`
- `perm_eq_mem` -> `perm_mem`
- `perm_eq_uniq` -> `perm_uniq`
- `perm_eq_rev` -> `perm_rev`
- `perm_eq_flatten` -> `perm_flatten`
- `perm_eq_all` -> `perm_all`
- `perm_eq_small` -> `perm_small_eq`
- `perm_eq_nilP` -> `perm_nilP`
- `perm_eq_consP` -> `perm_consP`
- `leq_size_perm` -> `uniq_min_size` (permuting conclusions)
- `perm_uniq` -> `eq_uniq` (permuting assumptions)
  --> beware `perm_uniq` now means `perm_eq_uniq`
- `uniq_perm_eq` -> `uniq_perm`
- `perm_eq_iotaP` -> `perm_iotaP`
- `perm_undup_count` -> `perm_count_undup`
- `tuple_perm_eqP` -> `tuple_permP`
- `eq_big_perm` -> `perm_big`
- `perm_eq_abelian_type` -> `abelian_type_pgroup`

### Misc

- removed Coq prelude hints `plus_n_O` `plus_n_Sm` `mult_n_O` `mult_n_Sm`,
  to improve robustness of `by ...`; scripts may need to invoke
  `addn0`, `addnS`, `muln0` or `mulnS`
  explicitly where these hints were used accidentally.

## [1.8.0] - 2019-04-08

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`

- support for casts in map comprehension notations, e.g.,
  `[seq E : T | s <- s]`.

- a predicate `all2`, a parallel double `seq` version of `all`.

- some `perm_eq` lemmas: `perm_cat[lr]`, `perm_eq_nilP`,
  `perm_eq_consP`, `perm_eq_flatten`.

- a function `permutations` that computes a duplicate-free list
  of all permutations of a given sequence `s` over an `eqType`, along
  with its theory: `mem_permutations`, `size_permutations`,
  `permutations_uniq`, `permutations_all_uniq`, `perm_permutations`.

- `eq_mktuple`, `eq_ffun`, `eq_finset`, `eq_poly`, `ex_mx` that can be
  used with the `under` tactic from the Coq 8.10 SSReflect plugin
  (cf. [coq/coq#9651](https://github.com/coq/coq/pull/9651))

### 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 the file `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`.
  + Replaced `allpairs_comp` with its converse `map_allpairs`.
  + Added `allpairs` extensionality lemmas for the following cases:
    non-localised (`eq_allpairs`), dependent localised
    (`eq_in_allpairs_dep`) and non-dependent localised
    (`eq_in_allpairs`); as per `eq_in_map`, the latter two are
    equivalences.

- Generalized `{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 non-dependent function type `A -> ?R` due to a bug in
  Coq version 8.9 or below.

- Renamed double `seq` induction lemma from `seq2_ind` to `seq_ind2`,
  and weakened its induction hypothesis.

- Replaced the `nosimpl` in `rev` with a `Arguments simpl never`
  directive.

- Many corrections in implicits declarations.

- fixed missing joins in `ssralg`, `ssrnum`, `finalg` and `countalg`

### 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`.

- Miscellaneous improvements to proof scripts and file organisation.

## [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