diff options
| author | Cyril Cohen | 2020-06-02 16:57:34 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-06 01:45:04 +0200 |
| commit | ccea59192ab383a9a0009d5ac5873e53f115c867 (patch) | |
| tree | 7e376f55fccf99a5a45b67ce346c9351c92ae3f0 /mathcomp/_CoqProject | |
| parent | 7f355343ee30f72d8ab3ce87f897dc0092e43c29 (diff) | |
Improvements
- deprecating `fintype.arg_(min|max)P`
- removing dangling comments connecting min max and meet join
- better compatibility module
- removing broken notations with `\min` and `\max` (no neutral available)
- fixing `incompare` and `incomparel` in order.v
- adding missing elimination lemmas (`(comparable_)?(max|min)E[lg][et]`)
- adding missing `(comparable|real)_arg(min|max)P`
- CHANGELOG update
Diffstat (limited to 'mathcomp/_CoqProject')
0 files changed, 0 insertions, 0 deletions