| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-31 | removing dead code + reshuffling stuff | Cyril Cohen | |
| 2018-07-31 | Rework the whole Makefile architecture | Cyril Cohen | |
| - Cleanup, refactoring and generalize the makefile architecture - Reuses @strub math-comp/analysis Makefile / Makefile.common organization - As #174, this fixes #88, but looks more stable than trying to fix the use of the MAKEFLAGS internal variable | |||
| 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 | |||
| 2017-11-14 | Update v8.5 plugin to fix math-comp/math-comp#61 | Erik Martin-Dorel | |
| 2017-06-09 | fix compilation on 8.5 | Enrico Tassi | |
| 2017-06-09 | fix compilation on 8.6 | Enrico Tassi | |
| 2017-06-07 | For trunk, use merged ssr plugin. | Maxime Dénès | |
| 2016-10-13 | Make: avoid >> Make, pass args to coq_makefile instead (#77) | Enrico Tassi | |
| 2016-06-16 | Port build system to trunk (ssrmatching merged in Coq) | Enrico Tassi | |
| 2016-01-21 | build script is now cygwin friendly | Enrico Tassi | |
| symlinks are not first class citizens on windows | |||
| 2015-07-29 | fix Makefiles | Enrico Tassi | |
| 2015-07-28 | factor common Makefile stuff | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |