| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-12-02 | take advantage of opam variables and their default values | Yves Bertot | |
| 2019-11-25 | Add Makefile target to build the doc | Maxime Dénès | |
| 2019-10-02 | Fix and improve the test suite and Makefile | Kazuhiko Sakaguchi | |
| - improve an error message produced by the `check_join` tactic, - fix the build of the test suite: `make test-suite`, and - add a new rule `only` to build a subset of MathComp. | |||
| 2019-04-30 | Reimplement the hierarchy related tools in OCaml | Kazuhiko Sakaguchi | |
| The functionalities of the structure hierarchy related tools `hierarchy-diagram` and `hierarchy_test.py` are provided by an OCaml script `hierarchy.ml`. `test_suite/hierarchy_test.v` is deleted. Now make can generate it. | |||
| 2019-04-08 | switching to opam 2.0 format | Cyril Cohen | |
| 2019-04-08 | New test cases generation: corrent implementation of least common children | Kazuhiko Sakaguchi | |
| Add a new option `-raw-inheritances` to `hierarchy-diagram` to generate an intermediate file for `hierarchy_test.py`. So the typical usage is: $ python3.5 etc/utils/hierarchy_test.py \ <(etc/utils/hierarchy-diagram -raw-inheritances -R mathcomp mathcomp) \ > mathcomp/test_suite/hierarchy_test.v | |||
| 2019-04-05 | least common childen | Cyril Cohen | |
| 2019-04-04 | no output on success in test_suite/hierarchy_test.v (#323) | Cyril Cohen | |
| 2019-04-02 | speedup in hierarchy_test.py | Cyril Cohen | |
| 2019-04-02 | identifying missing joins | Cyril Cohen | |
| 2019-03-07 | Put documentation and some command line options for hierarchy-diagram | Kazuhiko Sakaguchi | |
| 2019-03-07 | Use both coercions and canonical projections to generate the diagram | Kazuhiko Sakaguchi | |
| 2019-02-22 | Reimplement hierarchy-diagram by using coercions between "<module>.type" types | Kazuhiko Sakaguchi | |
| 2019-02-22 | Add a tool to draw the hierarchy diagram | Kazuhiko Sakaguchi | |
| 2019-02-05 | fix etc/utils/packager (#273) | Cyril Cohen | |
| 2018-04-24 | replacing my local `git root` by a universal command | Cyril Cohen | |
| 2018-04-24 | fix opam packager script + dependencies | Cyril Cohen | |
| 2018-04-20 | move etc/ files to the root and remove obsolete ones | Enrico Tassi | |
| 2017-10-23 | Remove compatibility with Coq.8.4 (and compatibility hacks that went with it) | Cyril Cohen | |
| 2017-10-23 | Merge pull request #145 from CohenCyril/new-packager | Cyril Cohen | |
| New packager | |||
| 2017-10-20 | reproduce github archive locally rather than downloading, much faster | Cyril Cohen | |
| 2017-10-20 | improved package generator | Cyril Cohen | |
| 2017-10-19 | new script to create opam meta packages | Cyril Cohen | |
| - the opam files in the branch where the script is launched should be correct - if not, the second argument to the script should be a branch in which the opam files are correct | |||
| 2017-10-19 | No more `cm*` files in the installer! | Enrico | |
| Since they are all in Coq! | |||
| 2017-09-07 | extended changelog in preparation for the next release | Cyril Cohen | |
| 2017-09-07 | adding odd_order to the list of released content for 1.6 | Cyril Cohen | |
| 2016-10-25 | minor change to the opam install example | Falcon Dai | |
| fix a typo in the example command add `opam repo add coq-released http://coq.inria.fr/opam/released` | |||
| 2016-08-25 | Enriched numClosedFieldType so that it factors a lot of theory from both ↵ | Cyril Cohen | |
| complex and algC. The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory have been moved to the numClosedFieldType structure in ssrnum. This covers boths the uses in algC and complex.v. To that end the numClosedFieldType structure has been enriched with conjugation and 'i. Note that 'i can be deduced from the property of algebraic closure and is only here to let the user chose which definitional equality should hold on 'i. Same thing for conjC that could be written `|x|^+2/x, the only nontrivial (up to my knowledge) property is the fact that conjugation is a ring morphism. | |||
| 2016-03-02 | Fix the address if the wiki. | Florent Hivert | |
| The previous fix wasn't right. | |||
| 2016-01-21 | revise installer for windows | Enrico Tassi | |
| 2016-01-05 | do not use `sed -i' in ssrcoqdep -- this is not portable | Pierre-Yves Strub | |
| This prevents compilation of ssreflect on OS-X/*BSD. | |||
| 2015-12-26 | packaging ssr 1.6 | Cyril Cohen | |
| 2015-12-18 | Changing the address of the wiki | amahboubi | |
| 2015-12-18 | Typo in the github announce | amahboubi | |
| 2015-12-15 | Update ANNOUNCE-1.6.md | Enrico | |
| 2015-12-14 | typo | Enrico Tassi | |
| 2015-12-14 | Update ANNOUNCE-github.md | Enrico | |
| 2015-12-12 | typo | Cyril Cohen | |
| 2015-12-12 | modif packager ":" -> "-" | Cyril Cohen | |
| 2015-12-11 | 8.5 coqdoc does not want _ to be escaped + more .css classes | Enrico Tassi | |
| 2015-12-10 | some doc for the doc building utility | Enrico Tassi | |
| 2015-12-09 | Updated the address of the website in README | Assia Mahboubi | |
| Plus corrected some typos. | |||
| 2015-12-09 | Moved comments on the incompatibility to INSTALL. | Assia Mahboubi | |
| Plus added a reference to the issue and the suggested solution in the other doc files. | |||
| 2015-12-08 | Create ANNOUNCE-github.md | Enrico | |
| First attempt to define the organization, please comment! | |||
| 2015-12-04 | Trying a better layout of hyperlinks on github | Assia Mahboubi | |
| 2015-12-04 | Trying a better layout of the .md on github | Assia Mahboubi | |
| 2015-12-04 | Minor edition of the Announce. | Assia Mahboubi | |
| Added a few more details in the description of the components and corrected some typos. | |||
| 2015-12-04 | Update ANNOUNCE-1.6.md | Enrico | |
| 2015-12-04 | better wording and package description in the ANNOUNCE for 1.6 | Enrico Tassi | |
| 2015-12-04 | some work on installation instructions and annoucement message | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |