| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-02-25 | fix compilation | Enrico Tassi | |
| 2016-02-25 | ssrpattern: compose nicely with Tactic Notation | Enrico Tassi | |
| 2016-02-22 | Guard "catch all" exception handler using Errors.noncritical | Enrico Tassi | |
| 2016-02-22 | rewrite: matching do not instantiate goal evars | Enrico Tassi | |
| 2016-02-22 | PF5: more predictable rewrite line (needed by rewrite using 8.5 refiner) | Enrico Tassi | |
| 2016-02-18 | typo in error message | thery | |
| 2016-02-18 | type in error message | thery | |
| 2016-02-15 | Removing compatibility layers. | Pierre-Marie Pédrot | |
| 2016-02-15 | Fixing ML compilation with trunk. | Pierre-Marie Pédrot | |
| 2016-02-09 | [div] Move dvdn_fact from prime to div. | Emilio Jesus Gallego Arias | |
| 2016-02-06 | typo in int divn1 -> divz1 | thery | |
| 2016-02-03 | Register flag "SsrHave NoTCResolution" in the Summary (fix #6) | Enrico Tassi | |
| 2016-02-03 | resolve type classes under the correct set of univs (fix #22) | Enrico Tassi | |
| 2016-02-02 | fix compilation on 8.4 | Enrico Tassi | |
| 2016-02-02 | Do not hide critical errors with a blind catch all (fix #19) | Enrico Tassi | |
| 2016-02-02 | fix debug print | Enrico Tassi | |
| 2016-02-02 | Explicit error message if rewrite fails due to TC inference (fix #21) | Enrico Tassi | |
| 2016-02-01 | compilation on trunk fixed | Enrico Tassi | |
| 2016-01-31 | Partially fixing ML compilation on trunk. | Pierre-Marie Pédrot | |
| 2016-01-31 | half-repair compilation on trunk | Enrico Tassi | |
| 2016-01-22 | generalizing odd_opp | Cyril Cohen | |
| 2016-01-21 | build script is now cygwin friendly | Enrico Tassi | |
| symlinks are not first class citizens on windows | |||
| 2016-01-12 | Move bullet initialization to ssreflect.v | Robbert Krebbers | |
| 2016-01-08 | fix version number in initialization message | Enrico Tassi | |
| 2015-12-26 | removing mathcomp dir when removing ssreflect | Cyril Cohen | |
| 2015-12-14 | fix compilation | Enrico Tassi | |
| 2015-12-13 | fix | Cyril Cohen | |
| 2015-12-12 | removing trailing whitespaces in opam file | Cyril Cohen | |
| 2015-12-12 | changing dependency | Cyril Cohen | |
| 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 | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |