coq-mathcomp/mathcomp/ssrtest, branch master Library of mathematical components formalized in Coq remove ssrtest: it now belongs to Coq 2018-04-12T07:54:36+00:00 Enrico Tassi 2018-04-12T07:54:36+00:00 d54b8dff818f0b1218df14cfb2b813da93154fa9 






Change Implicit Arguments to Arguments in odd_order
2018-02-22T09:57:03+00:00

Jasper Hugunin

2018-02-22T09:57:03+00:00

fe058c3300cf2385f1079fa906cbd13cd2349286












Merge pull request #177 from gares/fix/missing-ssrtest-in-Make
2018-02-21T14:10:05+00:00

Cyril Cohen

2018-02-21T14:10:05+00:00

13f26ccc09f87b222f9601892f085276a6ddb8c0

add 3 tests to Make




add 3 tests to Make






add 3 tests to Make
2018-02-06T14:46:26+00:00

Enrico Tassi

2018-02-06T12:52:29+00:00

3b2fd56a5645b3bd436085e514519c9f61200ae5












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












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







Change failing test.
2017-06-07T09:15:29+00:00

Maxime Dénès

2017-05-31T20:57:10+00:00

cd7ba12978ee90c2bf1e59584ebf95e9ed275fb2












ssrtest/elim.v: don't depend on Function
2017-03-23T14:09:50+00:00

Enrico Tassi

2017-03-23T14:09:50+00:00

caeeae8dcf76d494b20d7970b7e9e7022be96321

We inline the lemmas it generated, to ectly test the same thing
as before.





We inline the lemmas it generated, to ectly test the same thing
as before.







better test for primitive projections
2016-12-07T11:45:54+00:00

Enrico Tassi

2016-12-07T11:37:51+00:00

a369ebb35a13ea8b71d3960637937e6cde41211a