aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/order.v
AgeCommit message (Expand)Author
2021-03-08Adding big block matricesCyril Cohen
2021-03-07Adding Order.enum and related definitions and theoremsCyril Cohen
2021-01-16Drop support for Coq 8.10 and deprecate the `deprecate` notationKazuhiko Sakaguchi
2020-11-24Transpose `join_idP(l|r)` lemmas to follow the naming convention (#671)Kazuhiko Sakaguchi
2020-11-20Merge pull request #658 from CohenCyril/duplicate_clearaffeldt-aist
2020-11-20Removing unused cpo_sort scopeCyril Cohen
2020-11-19Removing duplicate clears and turning the warning into an errorCyril Cohen
2020-11-19add declare scopesReynald Affeldt
2020-11-13Rename `eq_sorted` lemmas to `sorted_eq` and generalize `sort_le_id`Kazuhiko Sakaguchi
2020-10-12Fixing and documenting the change of meaning of `>=< y`Cyril Cohen
2020-10-12Reorganizing relation between comparability/real and bigCyril Cohen
2020-10-12comparable_big lemma in order.vReynald Affeldt
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-09-17Fix big meet and join notations for dual_display, and add `0^d` and `1^d` not...Kazuhiko Sakaguchi
2020-09-05Adding contra lemmas with ordersCyril Cohen
2020-08-17Qualify the dual_* notations with the Order moduleKazuhiko Sakaguchi
2020-08-12Get rid of displays in class fields and mixin parametersKazuhiko Sakaguchi
2020-06-09add lua&sed to shell and switch to coq 8.11 + fixing docCyril Cohen
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-06Increasing definitional equalitiesCyril Cohen
2020-06-06Generalizing max and min to porderTypeCyril Cohen
2020-06-05Missing mono lemmas (#513)Cyril Cohen
2020-05-04Merge pull request #493 from pi8027/rm-tuple-lemmas-in-orderCyril Cohen
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
2020-04-09Merge pull request #474 from llelf/doc-typosaffeldt-aist
2020-04-08fix typos in documentation: textAntonio Nikishaev
2020-03-15Reorder arguments of comparison predicates in order.v as they shouldKazuhiko Sakaguchi
2020-03-15Extend comparison predicates for nat with minn and maxnKazuhiko Sakaguchi
2020-01-29Documentation work for (non-distributive) latticeTypeKazuhiko Sakaguchi
2020-01-15Non-distributive latticeKazuhiko Sakaguchi
2020-01-10Missing canonical structures for dualCyril Cohen
2020-01-10Exporting T^d notationCyril Cohen
2020-01-09Renaming converse to dual in order.vCyril Cohen
2019-12-28Refactoring and linting especially polydivKazuhiko Sakaguchi
2019-12-11Rephrasing the docCyril Cohen
2019-12-11Fix notation modifiers and scopesKazuhiko Sakaguchi
2019-12-11Doc, comments, changelog and better proofsCyril Cohen
2019-12-11Rename: (l|L)attice -> (d|D)istrLatticeKazuhiko Sakaguchi
2019-12-11Adding nat lattice under the name natdvdCyril Cohen
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:35:34 +0000