aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Expand)Author
2019-10-30Change the order of arguments in `ltngtP`Kazuhiko Sakaguchi
2019-10-26Add an explicit type annotation to GRing.scaleKazuhiko Sakaguchi
2019-10-25Removing duplicate lemma `addnKC` (= `addKn`)Cyril Cohen
2019-10-25Merge pull request #396 from CohenCyril/edivnDLaurent Théry
2019-10-25Instances for empty type. (#393)Arthur Azevedo de Amorim
2019-10-25Stability proofs of sort (#358)Kazuhiko Sakaguchi
2019-10-25More arithmetic theoremsCyril Cohen
2019-10-24Added and generalized arithmetic theorems. (#394)Cyril Cohen
2019-10-16renaming new `reindex_` lemmas with prefix `big_`Cyril Cohen
2019-10-16Improving fintype and bigopCyril Cohen
2019-10-14typothery
2019-10-07Merge pull request #384 from pi8027/hierarchyCyril Cohen
2019-10-05Add flatten_map1 and allpairs_consrKazuhiko Sakaguchi
2019-10-02Fix and improve the test suite and MakefileKazuhiko Sakaguchi
2019-09-30Generalize `allpairs_catr` to non-`eqType`sKazuhiko Sakaguchi
2019-09-30Euclid theorem for product (#375)Laurent Théry
2019-09-30ffact as a product similar to fact_prod (#374)Laurent Théry
2019-09-28maxn comment fix (#385)Antonio Nikishaev
2019-09-18Fix a typo: ring_core_scope -> ring_scopeKazuhiko Sakaguchi
2019-09-16fermat little theoremthery
2019-07-10totient for primethery
2019-07-05feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmasCyril Cohen
2019-06-18Merge pull request #340 from pi8027/hierarchyEnrico
2019-06-04Fixpoint theorems in finsetCyril Cohen
2019-05-29incorporate new suggestions by @CohenCyrilAnton Trunov
2019-05-29Replace eqVneq with eqPsymAnton Trunov
2019-05-29Canonical way of expressing dis-equality on an eqType is x != yAnton Trunov
2019-05-29Rename eqsP to eqPsym as suggested by @CohenCyrilAnton Trunov
2019-05-28Add eqsP view to destruct not only x == y, but also y == xAnton Trunov
2019-05-17refactor `seq` permutation theoryGeorges Gonthier
2019-05-08suppress use of `Arith` hintsSora Chen
2019-05-06add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma namesGeorges Gonthier
2019-04-30Ad-hoc fixKazuhiko Sakaguchi
2019-04-30Reimplement the hierarchy related tools in OCamlKazuhiko Sakaguchi
2019-04-30Fix compatibility for #237Georges Gonthier
2019-04-29reinstate token catenation hack in `prime.v`Georges Gonthier
2019-04-29Generalise use of `{pred T}` from coq/coq#9995Georges Gonthier
2019-04-26Cleaning Require and Require ImportsCyril Cohen
2019-04-24remove deprecated use of `if ... return`Georges Gonthier
2019-04-18Remove unused `Require`s and a hint directive from interval.vKazuhiko Sakaguchi
2019-04-17ssrnum doesn't use zmodpKazuhiko Sakaguchi
2019-04-08switching to opam 2.0 formatCyril Cohen
2019-04-08Merge pull request #318 from CohenCyril/hierarchy_testCyril Cohen
2019-04-08New test cases generation: corrent implementation of least common childrenKazuhiko Sakaguchi
2019-04-06Permutations and other extensions to seq; fintype documentationGeorges Gonthier
2019-04-06Fix inheritance bugs in finalg and extremalKazuhiko Sakaguchi
2019-04-04no output on success in test_suite/hierarchy_test.v (#323)Cyril Cohen
2019-04-04remove support for Coq 8.6Enrico Tassi
2019-04-03rename test-suite -> test_suite to make coq happyEnrico Tassi
2019-04-03Merge pull request #291 from pi8027/finalg-hierarchyCyril Cohen
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:59:38 +0000