aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-08Documenting addition policy to coq.Cyril Cohen
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-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
2020-05-04Remove the tuple extensions in order.v that is available in tuple.vKazuhiko Sakaguchi
2020-04-21Add dual_finLatticeType and fix dual_finDistrLatticeTypeKazuhiko Sakaguchi
This fixes two issues: - dual_finLatticeType was missing, and - dual_finDistrLatticeType was just an identity function.
2020-04-15fix packagerCyril Cohen
2020-04-15Merge pull request #487 from affeldt-aist/changelogs_release_1.11.0+beta1Yves Bertot
preparing changelogs to release 1.11.0+beta1
2020-04-15preparing changelogs to release 1.11.0+beta1Reynald Affeldt
2020-04-15Merge pull request #221 from hivert/permcomplaffeldt-aist
Some more lemmas on permutations
2020-04-15reworked new lemmas in perm and action and added missing onesCyril Cohen
In particular: rephrased permS0 and permS1 with all_equal_to
2020-04-15addressing comments about PR#221 of mathcompReynald Affeldt
2020-04-15Some more lemmas on permutationsFlorent Hivert
2020-04-15Merge pull request #475 from CohenCyril/ssrnat_deprecated_symbolsaffeldt-aist
adding deprecations in ssrnat
2020-04-10adding depreciations in ssrnatCyril Cohen
2020-04-10Merge pull request #471 from math-comp/all2_guard_condaffeldt-aist
Make `all2` better wrt the guard condition
2020-04-10Merge pull request #477 from affeldt-aist/move_good_practice_from_wikiCyril Cohen
Move the contents of Good Practices to CONTIBUTING.md
2020-04-10adding guard conditions check to the test_suiteCyril Cohen
2020-04-10Make `all2` better wrt the guard conditionCyril Cohen
fixes #469
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-12 10:36:44 +0000