| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-12 | Fixes doc of mxrepresentation.v | Florent Hivert | |
| 2016-05-04 | Merge pull request #40 from ppedrot/partial-fix | Enrico | |
| Fixing compilation after the merge of ML-tactic-notation branch. | |||
| 2016-05-02 | Fixing compilation after the merge of ML-tactic-notation branch. | Pierre-Marie Pédrot | |
| 2016-04-15 | Merge pull request #39 from ppedrot/partial-fix | Enrico | |
| Fixing compilation after the merge of PR trunk-function_scope. | |||
| 2016-04-08 | Fixing compilation after the merge of PR trunk-function_scope. | Pierre-Marie Pédrot | |
| 2016-03-31 | Merge pull request #38 from ppedrot/partial-fix | Enrico | |
| Fixing ML compilation. | |||
| 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 | Merge pull request #33 from ejgallego/search-print-with-msg | Enrico | |
| [search] Use msg_info to notify search results. | |||
| 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-03-02 | Merge pull request #32 from hivert/patch-1 | Yves Bertot | |
| Fix the address of the wiki. | |||
| 2016-03-02 | Fix the address if the wiki. | Florent Hivert | |
| The previous fix wasn't right. | |||
| 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 | Merge branch 'master' of https://github.com/math-comp/math-comp | thery | |
| 2016-02-18 | typo in error message | thery | |
| 2016-02-18 | type in error message | thery | |
| 2016-02-18 | type in error message | thery | |
| 2016-02-15 | Merge pull request #25 from ppedrot/partial-fix | Enrico | |
| Fixing ML compilation with trunk. | |||
| 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 | Merge pull request #24 from ejgallego/dvdn_fact | Assia Mahboubi | |
| [div] Move dvdn_fact from prime to div. | |||
| 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-02-01 | Merge pull request #20 from ppedrot/partial-fix | Enrico | |
| Partially fixing ML compilation on trunk. | |||
| 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-21 | revise installer for windows | Enrico Tassi | |
| 2016-01-12 | Move bullet initialization to ssreflect.v | Robbert Krebbers | |
| 2016-01-08 | fix version number in initialization message | Enrico Tassi | |
| 2016-01-06 | Merge pull request #13 from strub/master | Enrico | |
| do not use `sed -i' in ssrcoqdep -- this is not portable | |||
| 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 | removing mathcomp dir when removing ssreflect | Cyril Cohen | |
| 2015-12-26 | packaging ssr 1.6 | Cyril Cohen | |
| 2015-12-18 | Changing the address of the wiki | amahboubi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |