aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-18cardinality lemmas for #|A| <= 1 and n <= #|A|Christian Doczkal
2020-06-17Merge pull request #499 from chdoc/contra-propCyril Cohen
contra lemmas involving propositions
2020-06-17contra lemmas involving propositionsChristian Doczkal
2020-06-10Merge pull request #535 from CohenCyril/allow-coq-devCyril Cohen
Generated opam packages allow coq-dev again
2020-06-10Generated opam packages allow coq-dev againCyril Cohen
As a result of [a discussion on Zulip](https://coq.zulipchat.com/#narrow/stream/237665-math-comp-devs/topic/MathComp.201.2E11.2E0.20OPAM.20packages.20Coq.20compatibility) Reverts "removing opam `| (= "dev")` for released packages" (commit 313e44316177c918b363c118f15297e08d13eb4e).
2020-06-09removing opam `| (= "dev")` for released packagesCyril Cohen
2020-06-09Complying to SPDXCyril Cohen
2020-06-09fixing mailmapCyril Cohen
2020-06-09mailmap for Yves and ReynaldCyril Cohen
2020-06-09Merge pull request #533 from affeldt-aist/changelogs_before_releaseaffeldt-aist
edit changelogs before release
2020-06-09Merge pull request #534 from CohenCyril/doc-1.11Cyril Cohen
add lua&sed to nixshell and switch to coq 8.11 + fixing doc
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-10 21:54:58 +0000