| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-21 | Merge Arguments and Prenex Implicits | Anton Trunov | |
| See the discussion here: https://github.com/math-comp/math-comp/pull/242#discussion_r233778114 | |||
| 2018-10-31 | fixing local Makefile | Cyril Cohen | |
| should fix #238 | |||
| 2018-10-03 | [opam]: add dev-repo links | Anton Trunov | |
| This commit fixes the following issue: ```shell $ opam pin add coq-mathcomp-ssreflect --dev [ERROR] "dev-repo" field missing in coq-mathcomp-ssreflect metadata, you'll need to specify the pinning location ``` This commit also changes http to https for the homepage links. | |||
| 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-07-12 | Replace all the CoInductives with Variants | Kazuhiko Sakaguchi | |
| 2018-04-20 | fix symlinks to README, INSTALL and LICENSE | Enrico Tassi | |
| 2018-03-04 | Change deprecated Arguments Scope to Arguments | Jasper Hugunin | |
| 2018-02-21 | Change Implicit Arguments to Arguments in solvable | Jasper Hugunin | |
| 2018-02-06 | fixing things that @ggonthier and @ybertot spotted and some I spotted | Cyril Cohen | |
| 2018-02-06 | running semi-automated linting on the whole library | Cyril Cohen | |
| 2017-10-30 | Fix obsolete vernacular syntax for locality. | Maxime Dénès | |
| It was emitting a deprecation warning and will soon be removed from Coq. | |||
| 2017-10-23 | Remove compatibility with Coq.8.4 (and compatibility hacks that went with it) | Cyril Cohen | |
| 2017-10-23 | Merge pull request #145 from CohenCyril/new-packager | Cyril Cohen | |
| New packager | |||
| 2017-10-19 | fixed homepage | Cyril Cohen | |
| 2017-10-10 | fix building with make flags | Ralf Jung | |
| Fixes #139 | |||
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2016-10-24 | better ltngtP | Cyril Cohen | |
| 2015-12-12 | switch ":" to "-" | Cyril Cohen | |
| 2015-12-04 | Add elementary abelian finite modules lemmas to abelian | Georges Gonthier | |
| This factors proofs in mxabelem and finfield and removes dependencies between these two files. | |||
| 2015-12-04 | Removed spurious injection & clean up proof | Georges Gonthier | |
| 2015-11-10 | fix INSTALL symlinks | Enrico Tassi | |
| 2015-07-28 | update copyright banner | Enrico Tassi | |
| 2015-07-22 | remove duplicate fields | Cyril Cohen | |
| 2015-07-22 | make the opam package meta data | Cyril Cohen | |
| 2015-07-21 | update opam meta-data | Cyril Cohen | |
| 2015-07-18 | update to preserve backward compatibility with v8.4 | Cyril Cohen | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
| 2015-04-09 | adapting solvable to 8.5 | Cyril Cohen | |
| 2015-04-09 | Using the From X Require Y for v8.4 | Cyril Cohen | |
| 2015-04-08 | makefiles that are version dependent | Cyril Cohen | |
| 2015-03-24 | change finfield from field to character | Cyril Cohen | |
| 2015-03-24 | metadata for solvable and field | Cyril Cohen | |
| 2015-03-09 | Initial commit | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |