| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-11 | coqdoc + interactive graph browsing | Enrico Tassi | |
| It is still rough, but better than nothing. | |||
| 2015-12-11 | 8.5 coqdoc does not want _ to be escaped + more .css classes | Enrico Tassi | |
| 2015-12-10 | HACK: work around regression in 8.5 | Enrico Tassi | |
| This shall be reverted, it is there only to make ssr compile on jenkins and help the release of Coq | |||
| 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 | update license banner in .ml files | Enrico Tassi | |
| 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 | Merge branch 'master' of https://github.com/math-comp/math-comp | Georges Gonthier | |
| 2015-12-04 | Trailing whitespace removal | Georges Gonthier | |
| 2015-12-04 | Ignore emacs checkpoints | Georges Gonthier | |
| 2015-12-04 | Remove spurious injections | Georges Gonthier | |
| 2015-12-04 | Explicit construction of finite fields | Georges Gonthier | |
| Two lemmas provide splitting field for a given polynomials, and a finite field of a given (prime power) order, respectively. Internal comments document type-checking performance issues that arose. | |||
| 2015-12-04 | Some proof refactoring | Georges Gonthier | |
| 2015-12-04 | Move finfield to field module | Georges Gonthier | |
| 2015-12-04 | Add elementary abelian finite modules lemmas to abelian | Georges Gonthier | |
| This factors proofs in mxabelem and finfield and removes dependencies between these two files. | |||
| 2015-12-04 | Remove spurious injections | Georges Gonthier | |
| 2015-12-04 | Add instances & lemmas for regular algebras | Georges Gonthier | |
| 2015-12-04 | Document limitation of fieldExtType cloning | Georges Gonthier | |
| Default cloning requires a manifest field class. | |||
| 2015-12-04 | Correct improper CS declaration | Georges Gonthier | |
| Type cast on head constant spoils projection registration (Coq misfeature). | |||
| 2015-12-04 | Add finLmodType, finLalgType and finAlgType instances | Georges Gonthier | |
| 2015-12-04 | Removed spurious injection & clean up proof | Georges Gonthier | |
| 2015-12-04 | Remove more redundant power type structures | Georges Gonthier | |
| 2015-12-04 | Correct join values to baseFingroupType | Georges Gonthier | |
| These were all GRing.Zmodule.sort, instead of the corresponding sort in GRing (Ring.sort, Comin.sort, etc). | |||
| 2015-12-04 | Remove redundant structures for finite powers | Georges Gonthier | |
| 2015-12-04 | Add missing export | Georges Gonthier | |
| 2015-12-04 | fix coq-mathcomp-ssreflect opam package description | Enrico Tassi | |
| 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-12-03 | Removing the only use of globTacticIn. | Pierre-Marie Pédrot | |
| 2015-12-03 | add .mailmap to uniform names/email of committers | Enrico Tassi | |
| 2015-12-03 | fix compilation on trunk (thanks PMP) | Enrico Tassi | |
| 2015-12-03 | fix: autogen + abstract variables clash | Enrico Tassi | |
| 2015-12-03 | fix: elim/v handles eliminator from Derive Inversion (issue #2) | Enrico Tassi | |
| Also: - fix elim trying to saturate too much and not raising the expected exn - fix fill_occ_pattern when occ is {-}, it used to lose the instantiation obtained by matching the term | |||
| 2015-12-03 | Add commands to trace the matching algorithm | Enrico Tassi | |
| 2015-12-03 | fix: Hint View is not a Query | Enrico Tassi | |
| 2015-11-30 | Typos in comments. | Assia Mahboubi | |
| 2015-11-20 | Tested the Qed of the alternate Xirredp_FAdjoin in Coq 8.4. | Assia Mahboubi | |
| It's no more crashing but it's still way to long... | |||
| 2015-11-20 | Typo. | Assia Mahboubi | |
| 2015-11-20 | Typos | Assia Mahboubi | |
| 2015-11-10 | fix INSTALL symlinks | 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 | basic has disappeared | Cyril Cohen | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |