| Age | Commit message (Collapse) | Author |
|---|
|
- The `deprecate` notation and `iota_add` have been deprecated. All the uses of
the `deprecate` notation have been replaced with the `deprecated` attribute.
- Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1
have been removed.
- Remove `VDFILE` related hacks from `Makefile.common`.
|
|
|
|
|
|
|
|
This change reduces
- use of numerical occurrence selectors (#436) and
- use of non ssreflect tactics such as `auto`,
and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`,
`ltngtP`, and `eqVneq`.
|
|
+ `odd_add` -> `oddD`
+ `odd_sub` -> `oddB`
+ `take_addn` -> `takeD`
+ `rot_addn` -> `rotD`
+ `nseq_addn` -> `nseqD`
fixes #359
|
|
|
|
Replaced the legacy generalised induction idiom with a more robust one
that does not rely on the `{-2}` numerical occurrence selector, using
either new helper lemmas `ubnP` and `ltnSE` or a specific `nat`
induction principle `ltn_ind`.
Added (non-strict in)equality induction helper lemmas
Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression
along with some (in)equality, in preparation for some generalised
induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed
`ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember
that the inductive value remains below the initial one.
Used the change log to give notice to users to update the generalised
induction idioms in their proofs to one of the new forms before
Mathcomp 1.11.
|
|
In ssrnat:
- some trivial results in ssrnat `addnKC`, `ltn_predl`, `ltn_predr`, `ltn_subr` 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`
In div:
- 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: `modn_divl` and `divn_modl`.
- Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.
|
|
|
|
|
|
```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```
|
|
See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
|
|
|
|
|
|
|
|
|
|
|
|
|
