aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-04-01Merge pull request #735 from math-comp/nixHEADmasterCyril Cohen
Nix
2021-04-01update to last coq-nix-toolboxCyril Cohen
2021-03-25fix gotpodCyril Cohen
2021-03-24Merge pull request #728 from jouvelot/patch-1Kazuhiko Sakaguchi
Update path.v
2021-03-23Update mathcomp/ssreflect/path.v jouvelot
Sure. Thanks. Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
2021-03-23Update path.vjouvelot
Typo in documentation.
2021-03-18Merge pull request #707 from CohenCyril/ident_name_silenceCyril Cohen
Silencing warning deprecated-ident-entry
2021-03-17Merge pull request #725 from math-comp/nix_v2Cyril Cohen
Update nix CI
2021-03-17upCyril Cohen
2021-03-15update vscoq to 0.3.4Cyril Cohen
2021-03-15changing vscoq versionCyril Cohen
2021-03-15Merge pull request #723 from CohenCyril/gitpodCyril Cohen
fixup gitpod config
2021-03-15fixup gitpod configCyril Cohen
2021-03-14more gitpod config (#722)Cyril Cohen
2021-03-14Try gitpod (#721)Cyril Cohen
2021-03-14Adding sorting on tuples. (#720)jouvelot
* Adding sorting on tuples. Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2021-03-14Merge pull request #719 from CohenCyril/nix_v2Cyril Cohen
toolbox update
2021-03-14toolbox updateCyril Cohen
2021-03-12Silencing warning deprecated-ident-entryCyril Cohen
2021-03-12Merge pull request #717 from CohenCyril/nix_v2Cyril Cohen
toolbox update
2021-03-12toolbox updateCyril Cohen
2021-03-12Merge pull request #716 from CohenCyril/nix_v2Cyril Cohen
update nix toolbox
2021-03-12update nix toolboxCyril Cohen
2021-03-12Update nix toolbox version (#715)Cyril Cohen
* toolbox update * remove unnecessary step * update local shell version
2021-03-12Merge pull request #714 from math-comp/nix_v2Cyril Cohen
Use nix-tool-box
2021-03-12Use nix-tool-boxCyril Cohen
2021-03-12Revert "Use nix-tool-box"Cyril Cohen
This reverts commit 8674d6996fca76028ead3f75363f11bab4fa3e7c that I added by accident
2021-03-12Use nix-tool-boxCyril Cohen
2021-03-12Merge pull request #708 from CohenCyril/hint_locality_silenceCyril Cohen
Silencing Hint Locality warning
2021-03-08Merge pull request #703 from CohenCyril/blockmxLaurent Théry
Adding big block matrices
2021-03-08Adding big block matricesCyril Cohen
- with special cases for row, column, and diagonal matrices - we define an order bijection between the indexing of the whole matrix and the indexing of the blocks to preserve triangularity
2021-03-07Merge pull request #711 from math-comp/no-mc-devCyril Cohen
removing CI for analysis-dev
2021-03-07mathcomp analysis does not compire with Coq dev for nowCyril Cohen
2021-03-07Merge pull request #710 from CohenCyril/order_enumLaurent Théry
Adding Order.enum and related definitions and theorems
2021-03-07Adding Order.enum and related definitions and theoremsCyril Cohen
2021-03-04Silence Hint Locality warningCyril Cohen
2021-02-17Update nix.yml (#699)Cyril Cohen
* Update nix ci
2021-01-25Merge pull request #696 from CohenCyril/sumnBYves Bertot
Adding lemma sumnB
2021-01-22Merge pull request #686 from pi8027/drop-coq-8.10Cyril Cohen
Drop support for Coq 8.10
2021-01-22Remove deprecation aliases introduced in 1.9.0Kazuhiko Sakaguchi
2021-01-19Merge pull request #695 from affeldt-aist/interval_20210119Cyril Cohen
fixes #694
2021-01-19Update CHANGELOG_UNRELEASED.mdCyril Cohen
Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>
2021-01-19Adding lemma sumnBCyril Cohen
cf https://stackoverflow.com/questions/61556710
2021-01-19fixes #694Reynald Affeldt
2021-01-18Merge pull request #693 from affeldt-aist/interval_20210114Cyril Cohen
itv_bound comparison with -oo/+oo
2021-01-16Drop support for Coq 8.10 and deprecate the `deprecate` notationKazuhiko Sakaguchi
- The `deprecate` notation and `iota_add` have been deprecated. All the uses of the `deprecate` notation have been replaced with the `deprecated` attribute. - Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1 have been removed. - Remove `VDFILE` related hacks from `Makefile.common`.
2021-01-15Merge pull request #688 from pi8027/coq-8.13Cyril Cohen
[CI/CD] support Coq 8.13
2021-01-15[CI/CD] support Coq 8.13Kazuhiko Sakaguchi
2021-01-14itv_bound comparison with -oo/+ooReynald Affeldt
2021-01-13Update README.mdCyril Cohen
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 07:05:29 +0000