aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-25Adding lemma `oddS`Cyril Cohen
2020-08-20Merge pull request #550 from jashug/dont-refresh-argument-names-overlayEnrico Tassi
Be robust to a change in the default argument naming algorithm.
2020-08-17Merge pull request #547 from pi8027/qualified-dual-opCyril Cohen
Qualify the dual_* notations with the Order module
2020-08-17Qualify the dual_* notations with the Order moduleKazuhiko Sakaguchi
2020-08-16Merge pull request #517 from thery/minnCyril Cohen
Extra theorems about subn minn and maxn
2020-08-15Extra theorems about subn min and maxthery
2020-08-13Be robust to a change in the default argument naming algorithm.Jasper Hugunin
Overlay for coq/coq#12756, which changes the default argument name to just `S` from `S0`. This change preserves the old name; switching instead to use `S` may be preferable but introduces a potential impact on downstream users of mathcomp.
2020-08-13Merge pull request #545 from pi8027/fieldextCyril Cohen
Make [fieldExtType F of L] work for abstract instances
2020-08-13Merge pull request #553 from chdoc/non-reversible-notationCyril Cohen
fix non-reversible-notation warnings
2020-08-13Merge pull request #494 from pi8027/rm-displays-in-classesCyril Cohen
Get rid of displays in class fields and mixin parameters
2020-08-13fix non-reversible-notation warningsChristian Doczkal
2020-08-12Make [fieldExtType F of L] work for abstract instancesKazuhiko Sakaguchi
2020-08-12Get rid of displays in class fields and mixin parametersKazuhiko Sakaguchi
- In the definition of structures in order.v, displays are removed from parameters of mixins and fields of classes internally and now only appear in parameters of structures. Consequently, each mixin is now parameterized by a class rather than a structure, and the corresponding factory parameterized by a structure is provided to replace the use of the mixin. These factories have the same names as in the mixins before this change except that `bLatticeMixin` and `tbLatticeMixin` have been renamed to `bottomMixin` and `topMixin` respectively. - Added a factory `distrLatticePOrderMixin` in order.v to build a `distrLatticeType` from a `porderType`.
2020-08-11Merge pull request #552 from chdoc/rel-format-warningCyril Cohen
fix notation-incompatible-format warnings
2020-08-11fix notation-incompatible-format warningsChristian Doczkal
2020-08-11Merge pull request #507 from pi8027/test-guard-condCyril Cohen
Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition
2020-08-11Merge pull request #542 from chdoc/nothing-to-injectCyril Cohen
fix "Nothing to inject" warnings
2020-08-11Merge pull request #551 from CohenCyril/merge-changelog-by-unionCyril Cohen
Use union driver for CHANGELOG_UNRELEASED
2020-08-11Use union driver for CHANGELOG_UNRELEASEDCyril Cohen
2020-08-11Merge pull request #541 from chdoc/properCCyril Cohen
lemmas for proper and setC
2020-08-11Merge pull request #536 from pi8027/hierarchyCyril Cohen
Fix some hierarchy.ml related issues
2020-06-27Fix some Makefile issues and rename `hierarchy_test.v` to `test_hierarchy_all.v`Kazuhiko Sakaguchi
2020-06-27Fix bugs in hierarchy.mlKazuhiko Sakaguchi
- pass `Unix.environment ()` to `coqtop` to preserve the parent process environment, - check the exit status of `coqtop` and report an error if it is wrong, - do not rely on `ssrfun.id` in the `check_join` tactic, and - improve the error message for missing unification hints.
2020-06-26fix "Nothing to inject" warningsChristian Doczkal
2020-06-26lemmas for proper and setCChristian Doczkal
2020-06-24Merge pull request #540 from thery/docCyril Cohen
fix the doc for ubnP in ssrnat
2020-06-24Merge pull request #539 from thery/sum_nat_constCyril Cohen
simpler proof of sum_nat_const_nat in bigop.v
2020-06-24missing bigop lemmas (#537)Laurent Théry
* missing lemmas discovered while developing mathcomp-analysis Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr> * Intermediate lemmas and shortening proofs (thanks Laurent) Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr> Co-authored-by: Cyril Cohen <cohen@crans.org>
2020-06-24missing lemmas discovered while developing mathcomp-analysisReynald Affeldt
2020-06-24fix the doc for ubnP in ssrnatthery
2020-06-24simpler proofthery
2020-06-19Merge pull request #509 from chdoc/card-lemmasCyril Cohen
Card lemmas
2020-06-18conform to 80 chars limitChristian Doczkal
2020-06-18fixup spacingCyril Cohen
2020-06-18Apply suggestions from code reviewChristian Doczkal
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-06-18drop_uniq / CHANGELOGChristian Doczkal
2020-06-18add fcard_gt?P lemmas found in fourcolorChristian Doczkal
2020-06-18cards_eqP and cards2PChristian Doczkal
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-13Add more test cases for higher-order recursive functions in seq.v w.r.t. the ↵Kazuhiko Sakaguchi
guard condition
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:47:13 +0000