coq-mathcomp/mathcomp/real_closed, branch master Library of mathematical components formalized in Coq Moving real_closed to another repo 2018-04-18T08:49:18+00:00 Cyril Cohen 2018-04-17T15:00:15+00:00 13479422b0286c86d0888e06aba112153ca6314d 






Change deprecated Arguments Scope to Arguments
2018-03-05T00:57:06+00:00

Jasper Hugunin

2018-03-05T00:57:06+00:00

2525c33691e25f837b7dca31d4c702199b3dbc5d












Change Implicit Arguments to Arguments in real_closed
2018-02-22T09:45:41+00:00

Jasper Hugunin

2018-02-22T09:45:41+00:00

ddc1cc6857821220b9a67af0af042282200dbf44












fixing things that @ggonthier and @ybertot spotted and some I spotted
2018-02-06T13:14:36+00:00

Cyril Cohen

2018-02-06T13:04:50+00:00

f3ce9ace4b55654d6240db9eb41a6de3c488f0d9












running semi-automated linting on the whole library
2018-02-06T12:54:37+00:00

Cyril Cohen

2017-11-23T15:33:36+00:00

fafd4dac5315e1d4e071b0044a50a16360b31964












Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)
2017-10-23T13:54:07+00:00

Cyril Cohen

2017-10-23T13:52:09+00:00

dd730ed0569d57944435b6bb599bffd8c382c126












Merge pull request #145 from CohenCyril/new-packager
2017-10-23T09:24:50+00:00

Cyril Cohen

2017-10-23T09:24:50+00:00

f418fee13c770b27f2bf4fbfdfa2a1179596355e

New packager




New packager






fixed homepage
2017-10-19T20:17:14+00:00

Cyril Cohen

2017-10-19T20:17:14+00:00

42da1892c314e8faa545ce4657ec8633501eccd7












fix building with make flags
2017-10-10T11:23:30+00:00

Ralf Jung

2017-10-10T11:23:30+00:00

e888516870ef592d0f7da74f8138e478d6114b05

Fixes #139





Fixes #139







update copyright banner
2016-11-07T14:41:12+00:00

Assia Mahboubi

2016-11-07T14:40:31+00:00

2a8af6f6b80c82a5f07cae220427cccc30ef8dac