aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/algebra/ssrnum.v
AgeCommit message (Expand)Author
2021-01-16Drop support for Coq 8.10 and deprecate the `deprecate` notationKazuhiko Sakaguchi
2020-11-24Fix `@maxr` and `@minr`Kazuhiko Sakaguchi
2020-11-24Remove `Reserved Notation`s in `ssrnum.v` which are already declared in `orde...Kazuhiko Sakaguchi
2020-11-19Removing duplicate clears and turning the warning into an errorCyril Cohen
2020-11-18Merge pull request #599 from CohenCyril/dup_swap_applyEnrico Tassi
2020-11-12It is prohibited to use `exact:` in a `Hint Extern`Kazuhiko Sakaguchi
2020-11-11Intro pattern extensions for dup, swap and applyCyril Cohen
2020-10-29Merge pull request #605 from thery/bigopKazuhiko Sakaguchi
2020-10-12fix the >=< notation in ssrnum as wellReynald Affeldt
2020-10-12Reorganizing relation between comparability/real and bigCyril Cohen
2020-10-12comparable_big lemma in order.vReynald Affeldt
2020-10-12lemma used in mathcomp-analysisReynald Affeldt
2020-10-10Adding bigop lemmas for ring : expr_sum and prodr_natmulthery
2020-10-07Turn class_of records into primitive records and get rid of the xclass idiomKazuhiko Sakaguchi
2020-09-28Apply suggestions from code reviewKazuhiko Sakaguchi
2020-08-12Get rid of displays in class fields and mixin parametersKazuhiko Sakaguchi
2020-06-24missing lemmas discovered while developing mathcomp-analysisReynald Affeldt
2020-06-09fix coq 8.12 warningsCyril Cohen
2020-06-06ImprovementsCyril Cohen
2020-06-06tentative changelogReynald Affeldt
2020-06-06General theory of min and max, and use in ssrnumCyril Cohen
2020-06-05fix namingReynald Affeldt
2020-06-04fix namingReynald Affeldt
2020-06-03add real_* variantsReynald Affeldt
2020-06-02another lemma about norm from mathcomp-analysisReynald Affeldt
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
2020-04-06Some proof scripts made better using ssrAC.Cyril Cohen
2020-04-01Merge pull request #429 from pi8027/extend-nat-comparisonYves Bertot
2020-03-15just noticed a tentative use of a not yet existing lemmaReynald Affeldt
2020-03-15Reorder arguments of comparison predicates in order.v as they shouldKazuhiko Sakaguchi
2020-01-15Non-distributive latticeKazuhiko Sakaguchi
2019-12-28Refactoring and linting especially polydivKazuhiko Sakaguchi
2019-12-11The compatibility module in ssrnum should now be for version 1.10Kazuhiko Sakaguchi
2019-12-11remove ProdNormedZmodule (#419)affeldt-aist
2019-12-11renaming NormedZmoduleType and NormedZmoduleMixin (#416)affeldt-aist
2019-12-11Fix notation modifiers and scopesKazuhiko Sakaguchi
2019-12-11Comparability in a numDomainTypeCyril Cohen
2019-12-11Rename: (l|L)attice -> (d|D)istrLatticeKazuhiko Sakaguchi
2019-12-11editing documentation in order.v and ssrnum.vReynald Affeldt
2019-12-11order.v: remove Order.Def, export Order.Syntax by default, and put missing sc...Kazuhiko Sakaguchi
2019-12-11Redefine `normedDomainType` (now `normedZmodType`) (#392)Kazuhiko Sakaguchi
2019-12-11Rename `totalLatticeMixin` to `totalPOrderMixin` and several refactorKazuhiko Sakaguchi
2019-12-11Add (meet|join)_(l|r), some renamings, and small cleanupsKazuhiko Sakaguchi
2019-12-11Reorder the arguments of the comparison predicates in order.vKazuhiko Sakaguchi
2019-12-11Fixes in naming, mixins, doc and canonical orderingCyril Cohen
2019-12-11Use `deprecate` notation in ssrnumKazuhiko Sakaguchi
2019-12-11Make an appropriate use of the order library everywhere (#278, #280, #282, #2...Kazuhiko Sakaguchi
2019-12-11Initial import of order.v into mathcompCohen Cyril
2019-11-22New generalised induction idiom (#434)Georges Gonthier
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:05:58 +0000