| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-26 | Add ssrmatching.v transitional file | Erik Martin-Dorel | |
| The content of this file is similar to that of ssrfun.v and aims to increase compatibility with Coq 8.6+ for third-party libraries that depend on both math-comp and ssrmatching.v Close #63 | |||
| 2018-02-06 | add 3 tests to Make | Enrico Tassi | |
| 2017-06-07 | For trunk, use merged ssr plugin. | Maxime Dénès | |
| 2016-12-07 | new test for "rewrite /x" when x is Opaque | Enrico Tassi | |
| 2016-12-06 | add test for unfolding primitive projections | Enrico Tassi | |
| 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-02-25 | ssrpattern: compose nicely with Tactic Notation | Enrico Tassi | |
| 2015-12-04 | Move finfield to field module | Georges Gonthier | |
| 2015-11-05 | merge basic/ into ssreflect/ | Enrico Tassi | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |