aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-11Merge pull request #302 from CohenCyril/fixsetGeorges Gonthier
2019-06-04Fixpoint theorems in finsetCyril Cohen
2019-05-29Merge pull request #353 from anton-trunov/update-ciCyril Cohen
2019-05-29Replace eqVneq to destruct both x == y, but also y == x (#351)Cyril Cohen
2019-05-29Remove support for Travis CIAnton Trunov
2019-05-29Update pull_request_template.mdCyril Cohen
2019-05-29Merge pull request #352 from CohenCyril/pr_tempateCyril Cohen
2019-05-29reword entry in CHANGELOG_UNRELEASED.mdAnton Trunov
2019-05-29Update pull_request_template.mdCyril Cohen
2019-05-29Move unreleased changelog entries to CHANGELOG_UNRELEASED.mdAnton Trunov
2019-05-29pr templateCyril 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-22htmldoc regeneratedEnrico Tassi
2019-05-22typoEnrico
2019-05-22Update CHANGELOG.mdGeorges Gonthier
2019-05-22Update INSTALL.mdEnrico
2019-05-22be explicit about opam version 2.xEnrico
2019-05-22Update README.mdCyril Cohen
2019-05-21Update CHANGELOG.mdCyril Cohen
2019-05-17Merge pull request #345 from math-comp/perm-tallyGeorges Gonthier
2019-05-17refactor `seq` permutation theoryGeorges Gonthier
2019-05-08Merge pull request #344 from soraros/ssrnat-remove-arith-lemmasGeorges Gonthier
2019-05-08suppress use of `Arith` hintsSora Chen
2019-05-06Merge pull request #342 from math-comp/deprecationGeorges Gonthier
2019-05-06add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma namesGeorges Gonthier
2019-04-30Merge pull request #339 from math-comp/coq-ssrbool-refactor-compatGeorges Gonthier
2019-04-30Restore CI with `finmap master`Georges Gonthier
2019-04-30Merge pull request #338 from math-comp/coq-ssrbool-refactor-compatGeorges Gonthier
2019-04-30Fix compatibility for #237Georges Gonthier
2019-04-29Merge pull request #337 from math-comp/coq-ssrbool-refactor-compatGeorges 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-28Merge pull request #336 from CohenCyril/clean_requireGeorges Gonthier
2019-04-26Cleaning Require and Require ImportsCyril Cohen
2019-04-25Merge pull request #335 from math-comp/fix-if-returnGeorges Gonthier
2019-04-24remove deprecated use of `if ... return`Georges Gonthier
2019-04-23Merge pull request #332 from pi8027/zmodp-intervalCyril Cohen
2019-04-18Remove unused `Require`s and a hint directive from interval.vKazuhiko Sakaguchi
2019-04-18Merge pull request #331 from pi8027/zmodp-ssrnumCyril Cohen
2019-04-17ssrnum doesn't use zmodpKazuhiko Sakaguchi
2019-04-17Merge pull request #307 from erikmd/extend-ciCyril Cohen
2019-04-17Merge pull request #306 from erikmd/refactor-ciCyril Cohen
2019-04-16[ci] Add tests with more librariesErik Martin-Dorel
2019-04-16Detail: Print a more legible description for the cloned external librariesErik Martin-Dorel
2019-04-16Don't run "opam clean -c" to workaround ocaml/opam#3828Erik Martin-Dorel
2019-04-16Swap the deploy and test stagesErik Martin-Dorel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 17:11:23 +0000