| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-12 | Merge pull request #43 from hivert/fixdoc | Georges Gonthier | |
| Fixes the doc of mxrepresentation.v | |||
| 2016-05-12 | Fixes doc of mxrepresentation.v | Florent Hivert | |
| 2016-05-09 | Fix compilation after the merge of the dynamic tactic value branch. | Pierre-Marie Pédrot | |
| 2016-05-02 | Fixing compilation after the merge of ML-tactic-notation branch. | Pierre-Marie Pédrot | |
| 2016-04-08 | Fixing compilation after the merge of PR trunk-function_scope. | Pierre-Marie Pédrot | |
| 2016-03-27 | Fixing ML compilation. | Pierre-Marie Pédrot | |
| 2016-03-15 | Merge pull request #34 from strub/master | Enrico | |
| all_algebra now exports zmodp | |||
| 2016-03-15 | all_algebra now exports zmodp | Pierre-Yves Strub | |
| 2016-03-03 | [search] Use msg_info to notify search results. | Emilio Jesus Gallego Arias | |
| By default, the search command calls `Pp.msg` to print search results. Unfortunately, this bypasses the `log_via_feedback` option and produces not very nice results on feedback-depending IDES like JsCoq. A proper fix would involve merging coq/coq#143 , and the upcoming search cleanup, but this should do the trick for now. I couldn't observe any problem with the usual testing. | |||
| 2016-03-03 | fix local opam file | Cyril Cohen | |
| 2016-03-02 | fix compilation of ssrmatching in trunk | Enrico Tassi | |
| 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 | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |