| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-06-17 | this test is now in Coq, removing it. | Enrico Tassi | |
| 2016-06-16 | Port build system to trunk (ssrmatching merged in Coq) | Enrico Tassi | |
| 2016-06-03 | Merge pull request #49 from matej-kosik/master | Enrico | |
| fixing compilation (with Coq trunk & Coq v8.5) | |||
| 2016-06-03 | fixing compilation (with Coq trunk & Coq v8.5) | Matej Kosik | |
| 2016-06-01 | Merge pull request #48 from ejgallego/pp_cleanup_fix | Enrico | |
| Compatibility with latest Coq trunk. | |||
| 2016-05-31 | Compatibility with latest Coq trunk. | Emilio Jesus Gallego Arias | |
| 2016-05-18 | Merge pull request #46 from ppedrot/partial-fix | Enrico | |
| Fix compilation after the change of API in Tactics. | |||
| 2016-05-18 | Fix compilation after the change of API in Tactics. | Pierre-Marie Pédrot | |
| 2016-05-16 | Merge pull request #44 from ppedrot/partial-fix | Enrico | |
| Fix compilation after the renaming of Lexer into CLexer. | |||
| 2016-05-16 | Fix compilation after the renaming of Lexer into CLexer. | Pierre-Marie Pédrot | |
| 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 | Merge pull request #42 from ppedrot/partial-fix | Enrico | |
| Fix compilation after the merge of the dynamic tactic value branch. | |||
| 2016-05-09 | Fix compilation after the merge of the dynamic tactic value branch. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |