aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-30Ad-hoc fixKazuhiko Sakaguchi
2019-04-30Reimplement the hierarchy related tools in OCamlKazuhiko Sakaguchi
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
2019-04-16Print more debug informationErik Martin-Dorel
2019-04-16Refactor jobs: Split .opam-build & Create .docker-deployErik Martin-Dorel
2019-04-16Add commentary sections & Swap order of .make-build, .opam-buildErik Martin-Dorel
2019-04-08Merge pull request #325 from CohenCyril/opam-2.0Cyril Cohen
2019-04-08Update CHANGELOG.mdCyril Cohen
2019-04-08Update CHANGELOG.mdCyril Cohen
2019-04-08update mailmapEnrico Tassi
2019-04-08switching to opam 2.0 formatCyril Cohen
2019-04-08Update INSTALL.mdCyril Cohen
2019-04-08Update CHANGELOG.mdCyril Cohen
2019-04-08Merge pull request #318 from CohenCyril/hierarchy_testCyril Cohen