aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-09add lua&sed to shell and switch to coq 8.11 + fixing docCyril Cohen
2020-06-09edit changelogs before releaseReynald Affeldt
2020-06-09Merge pull request #532 from CohenCyril/silence-8.12-warningsCyril Cohen
fix coq 8.12 warnings
2020-06-09fix coq 8.12 warningsCyril Cohen
2020-06-08Merge pull request #531 from CohenCyril/fix_cyclotomicCyril Cohen
turning let into local definition
2020-06-08turning let into local definitionCyril Cohen
2020-06-08More CICyril Cohen
- fourcolor 8.11 and 8.12 - odd-order 8.11 and 8.12 - bigenough 8.11 and 8.12 - finmap 8.11 and 8.12
2020-06-08Merge pull request #528 from CohenCyril/silence_warningsCyril Cohen
silencing warnings in individual packages
2020-06-08silencing warnings in individual packagesCyril Cohen
2020-06-08Merge pull request #519 from CohenCyril/homomono_inYves Bertot
Missing homo/mono lemmas in the presence of cancellation
2020-06-08Cachix action (#525)Cyril Cohen
tentative fix
2020-06-08Documenting addition policy to coq.Cyril Cohen
2020-06-08Merge pull request #524 from erikmd/coq-8.12Cyril Cohen
[CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha)
2020-06-07[CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha)Erik Martin-Dorel
2020-06-06Merge pull request #522 from affeldt-aist/update_readmeCyril Cohen
change links to the wiki to links to the website
2020-06-06bugfixCyril Cohen
2020-06-06fix the changelogReynald Affeldt
2020-06-06add new lemmas to the changelogReynald Affeldt
2020-06-06Missing homo_mono lemmasCyril Cohen
2020-06-06Merge pull request #516 from CohenCyril/maxraffeldt-aist
Generalizing max and min to porderType
2020-06-06ImprovementsCyril Cohen
- 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
2020-06-06tentative changelogReynald Affeldt
- mostly gathered the changes from previous commits - add `minrC` - minor doc addition to `order.v`
2020-06-06General theory of min and max, and use in ssrnumCyril Cohen
- min and max can now be used in a partial order (sometimes under preconditions) - min and max can now be used in a numDomainType (sometimes under preconditions)
2020-06-06Increasing definitional equalitiesCyril Cohen
- `Order.max` and `Order.min` are now convertible to `maxn` and `minn` - Inserting `(fun _ _ => erefl)` in `LeOrderMixin` and `LtOrderMixin` gives `meet`/`join` which are convertible to `min`/`max` - `Order.max` and `Order.min` are not convertible to former `Num.max` and `Num.min`
2020-06-06Generalizing max and min to porderTypeCyril Cohen
- max and min are not defined in terms or meet and join anymore - extremum_inP is a generalization of extremum suitable for a partial order - arg_min and arg_max are usable in a porderType - equivalences between min and meet, and max and join are proven for orderType - leP, ltP, ltgtP, and `[l]?comparable_.*P` lemmas have been generalized to take this into account - total_display was completely removed
2020-06-06change links to the wiki to links to the websiteReynald Affeldt
2020-06-05Merge pull request #514 from affeldt-aist/lemmas_from_analysis_20200521Yves Bertot
Lemma addition to ssrnum
2020-06-05fix namingReynald Affeldt
2020-06-05Missing mono lemmas (#513)Cyril Cohen
* Missing mono lemmas
2020-06-04fix changelogReynald Affeldt
2020-06-04fix md formattingReynald Affeldt
2020-06-04fix namingReynald Affeldt
2020-06-03Merge pull request #520 from CohenCyril/cachix-actionCyril Cohen
Cachix action
2020-06-03update default nix and setup cachixCyril Cohen
2020-06-03add real_* variantsReynald Affeldt
2020-06-02another lemma about norm from mathcomp-analysisReynald Affeldt
2020-05-28Merge pull request #511 from CohenCyril/nixYves Bertot
adding default nix shell
2020-05-28Merge pull request #504 from pi8027/selectorsaffeldt-aist
Revise proofs in ssreflect/*.v
2020-05-27URL in httpsCyril Cohen
2020-05-22tentative change of naming convention and add variantsReynald Affeldt
2020-05-21three lemmas that we found useful in the context of theReynald Affeldt
mathcomp-analysis project
2020-05-16A few more revisionsKazuhiko Sakaguchi
2020-05-15adding default nix shellCyril Cohen
2020-05-13Revise proofs in ssreflect/*.vKazuhiko Sakaguchi
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`.
2020-05-06Merge pull request #495 from pi8027/post-cleaning-pr429Cyril Cohen
Reword a CHANGELOG entry introduced in #429
2020-05-06Reword a CHANGELOG entry introduced in #429Kazuhiko Sakaguchi
that explains an incompatibility between development versions
2020-05-04Merge pull request #498 from chdoc/doc-in-memCyril Cohen
document 'in_' and 'mem_' prefixes for infix membership
2020-05-04document 'in_' and 'mem_' prefixes for infix membershipChristian Doczkal
2020-05-04Merge pull request #493 from pi8027/rm-tuple-lemmas-in-orderCyril Cohen
Remove the tuple extensions in order.v that is available in tuple.v
2020-05-04Merge pull request #490 from pi8027/fix-fin-dual-orderCyril Cohen
Add dual_finLatticeType and fix dual_finDistrLatticeType
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:53:18 +0000