| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-12 | switch ":" to "-" | Cyril Cohen | |
| 2015-12-12 | fixing requires in stripped odd order | Cyril Cohen | |
| 2015-12-12 | Revert "HACK: work around regression in 8.5" | Enrico Tassi | |
| This reverts commit 006565bdb5b473afff5f834e4b20320bb0a419fd. since Coq commit c6b75e1b693ab8c7af2efd1b93f04eab248e584c make this unnecessary | |||
| 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-04 | update license banner in .ml files | Enrico Tassi | |
| 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 | 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-03 | Removing the only use of globTacticIn. | Pierre-Marie Pédrot | |
| 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-06 | basic has disappeared | Cyril Cohen | |
| 2015-11-05 | merge basic/ into ssreflect/ | Enrico Tassi | |
| 2015-10-26 | Added support for highlighting 'isn't' in PG. | Assia Mahboubi | |
| 2015-10-26 | Added suport for highlighting gen(erally) have in PG. | Assia Mahboubi | |
| 2015-10-26 | Small updates in the documentation of the customization of PG. | Assia Mahboubi | |
| 2015-10-26 | Restaured the config files (including doc) for PG in the ssreflect package. | Assia Mahboubi | |
| 2015-09-27 | fix compilation on trunk | Enrico Tassi | |
| 2015-09-24 | Fix compilation on 8.5 | Enrico Tassi | |
| 2015-08-24 | Compare pattern heads (constants) up to "univs" | Enrico Tassi | |
| So that Universe Polymorphic constants are compared "correctly", i.e. not discriminated by the pattern filtering phase (verbatim head comparison) but eventually by unification. | |||
| 2015-07-30 | fix trunk compilation | Enrico Tassi | |
| 2015-07-29 | fix PF | Cyril Cohen | |
| 2015-07-29 | add a missing From ... | Cyril Cohen | |
| 2015-07-29 | fix Makefiles | Enrico Tassi | |
| 2015-07-29 | fix path of Makefile.coq-makefile | Enrico Tassi | |
| 2015-07-28 | update copyright banner | Enrico Tassi | |
| 2015-07-28 | factor common Makefile stuff | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |