| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-03-21 | Merge pull request #108 from ejgallego/pp_new_fix | Maxime Dénès | |
| Use pp_with as msg_with is being removed upstream. | |||
| 2017-03-13 | Reflection lemmas for `seq.uniq` | Pierre-Yves Strub | |
| 2017-02-23 | [safe-string] Allow compilation with -safe-string. | Emilio Jesus Gallego Arias | |
| The first part of changes is easy, we could maybe polish the notation part a bit more. | |||
| 2017-02-21 | Use pp_with as msg_with is being removed upstream. | Emilio Jesus Gallego Arias | |
| 2017-02-21 | Compatiblity with Ltac as a plugin. | Maxime Dénès | |
| 2017-02-07 | remove documentation for subfilter. | Tanaka Akira | |
| subfilter was exist at ssreflect-1.1 and removed at ssreflect-1.2. | |||
| 2016-12-20 | correct a typo in the documentation | Yves Bertot | |
| 2016-12-19 | fix compilation on 8.5 | Enrico Tassi | |
| 2016-12-06 | backport Coq PR#387 on ssrmatching for Coq v8.5 | Enrico Tassi | |
| 2016-12-06 | Use Tacred.unfoldn [AllOccurrences..] to work around Coq #5250 | Enrico Tassi | |
| 2016-12-06 | rewrite /primitive_projection is now supported (fix #85) | Enrico Tassi | |
| 2016-11-08 | fix compilation on 8.6 and trunk | Enrico Tassi | |
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2016-10-24 | removing the need of bracket to delimit ssrpatternarg | Cyril Cohen | |
| 2016-10-24 | better ltngtP | Cyril Cohen | |
| 2016-10-13 | Make: avoid >> Make, pass args to coq_makefile instead (#77) | Enrico Tassi | |
| 2016-10-13 | Merge pull request #65 from gares/master | Cyril Cohen | |
| abstract_context utility lemma | |||
| 2016-10-13 | Merge pull request #66 from thery/master | Cyril Cohen | |
| Adding theorems in binomial | |||
| 2016-10-12 | changing "ssreflect.ml4" so that we avoid triggering bugs in camlp5's ↵ | Matej Kosik | |
| "pr_o.cmo" plugin | |||
| 2016-10-05 | Generalization in the type of contra_eq/contra_neq. | Assia Mahboubi | |
| Thanks B. Grégoire for this suggestion. | |||
| 2016-09-27 | Add a typing colon in the output of the Search ssreflect vernacular. | Erik Martin-Dorel | |
| 2016-09-24 | Fix ML compilation after Ltac refactoring. | Pierre-Marie Pédrot | |
| 2016-09-23 | FIX: compilation wrt. commit 9c35248 on Coq trunk branch. | Matej Kosik | |
| 2016-09-22 | fix compilation wrt. commit 699b70c in Coq trunk | Matej Kosik | |
| 2016-09-16 | Refactoring of binonial | thery | |
| Variable renaming from 'C(m,n) to 'C(n,m) Renaming theorem mul_Sm_binn to mul_bin_diag Adding theorems mul_bin_left mul_bin_right | |||
| 2016-09-16 | Fix compilation after change in CErrors API. | Pierre-Marie Pédrot | |
| 2016-09-07 | fix comment | Enrico | |
| 2016-09-07 | abstract_context utility lemma | Enrico | |
| 2016-08-26 | fix compilation wrt. commit 69388fc in Coq trunk | Matej Kosik | |
| 2016-08-25 | FIX: adding missing version of the ssreflect plugin that compiles with Coq v8.6. | Matej Kosik | |
| The committed files represent copies of the ssreflect plugin for Coq trunk taken from commit c353aa5 which is the last commit in which ssreflect plugin marked for Coq trunk is usable with both, Coq trunk as well as Coq v8.6. | |||
| 2016-08-24 | Possible code compaction motivated by Enrico's remark: ↵ | Matej Kosik | |
| https://github.com/math-comp/math-comp/pull/58#discussion_r76048943 | |||
| 2016-08-17 | Removing calls of "Context.Named.Declaration.to_tuple" function | Matej Kosik | |
| 2016-08-17 | use a convenient module alias instead of "Context.Rel.Declaration" and ↵ | Matej Kosik | |
| "Context.Named.Declaration" | |||
| 2016-08-16 | fix compilation on trunk (thanks Matej) | Enrico Tassi | |
| 2016-07-03 | Fix compilation after Errors and Closure were renamed. | Maxime Dénès | |
| 2016-07-01 | Fix compilation after renaming of reduction functions and flags in Coq. | Maxime Dénès | |
| 2016-06-16 | Port build system to trunk (ssrmatching merged in Coq) | Enrico Tassi | |
| 2016-06-03 | fixing compilation (with Coq trunk & Coq v8.5) | Matej Kosik | |
| 2016-05-31 | Compatibility with latest Coq trunk. | Emilio Jesus Gallego Arias | |
| 2016-05-18 | Fix compilation after the change of API in Tactics. | Pierre-Marie Pédrot | |
| 2016-05-16 | Fix compilation after the renaming of Lexer into CLexer. | Pierre-Marie Pédrot | |
| 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-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 | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |