coq-mathcomp/mathcomp/odd_order, branch masterLibrary of mathematical components formalized in Coqmove odd_order to its own repository2018-04-17T14:57:13+00:00Enrico Tassi2018-04-17T14:57:13+00:00eaa90cf9520e43d0b05fc6431a479e6b9559ef0e
Change deprecated Arguments Scope to Arguments2018-03-05T00:57:06+00:00Jasper Hugunin2018-03-05T00:57:06+00:002525c33691e25f837b7dca31d4c702199b3dbc5d
Change Implicit Arguments to Arguments in odd_order2018-02-22T09:57:03+00:00Jasper Hugunin2018-02-22T09:57:03+00:00fe058c3300cf2385f1079fa906cbd13cd2349286
fixing things that @ggonthier and @ybertot spotted and some I spotted2018-02-06T13:14:36+00:00Cyril Cohen2018-02-06T13:04:50+00:00f3ce9ace4b55654d6240db9eb41a6de3c488f0d9
running semi-automated linting on the whole library2018-02-06T12:54:37+00:00Cyril Cohen2017-11-23T15:33:36+00:00fafd4dac5315e1d4e071b0044a50a16360b31964
Fix the only remaining spurious injection in the entire codebase.2017-11-06T16:18:44+00:00Maxime Dénès2017-11-06T16:15:35+00:00c2a42557d0cc7c4c776a4572dcfeef011bfc73b8
We may want to make it an error, now that the transition period has been
long enough.
We may want to make it an error, now that the transition period has been
long enough.
Fix obsolete vernacular syntax for locality.2017-10-30T13:16:48+00:00Maxime Dénès2017-10-30T13:16:48+00:00e1b1743fb6aaed042d5e6762ea76c3242593ab1d
It was emitting a deprecation warning and will soon be removed from Coq.
It was emitting a deprecation warning and will soon be removed from Coq.
Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)2017-10-23T13:54:07+00:00Cyril Cohen2017-10-23T13:52:09+00:00dd730ed0569d57944435b6bb599bffd8c382c126
Merge pull request #145 from CohenCyril/new-packager2017-10-23T09:24:50+00:00Cyril Cohen2017-10-23T09:24:50+00:00f418fee13c770b27f2bf4fbfdfa2a1179596355e
New packager