| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-11-10 | Adding sections for definitions in change log | amahboubi | |
| 2015-11-10 | Update ChangeLog | amahboubi | |
| 2015-11-09 | ChangeLog: yake Yves' suggestion into account | Enrico | |
| 2015-11-06 | First stab at INSTALL | Enrico Tassi | |
| 2015-11-06 | Makefile to create a tar ball | Enrico Tassi | |
| 2015-11-05 | Changelog file created | Enrico Tassi | |
| 2015-07-22 | opam meta-data +url | Cyril Cohen | |
| 2015-07-22 | make the opam package meta data | Cyril Cohen | |
| 2015-07-21 | make opam meta-data | Cyril Cohen | |
| 2015-07-21 | patch ssrcoqdep | Cyril Cohen | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
| 2015-03-09 | some work on ssreflect and discrete | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |