| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 |