coq-mathcomp/mathcomp/test_suite, branch master Library of mathematical components formalized in Coq Using `only printing` and fixing coercion in notations 2020-11-25T18:26:22+00:00 Cyril Cohen 2020-11-24T22:14:22+00:00 9c693eedb8e7e11aeaedbd3ce79a9478b10be7c8 






fixing [dup] for Coq 8.12
2020-11-23T21:49:11+00:00

Cyril Cohen

2020-11-23T16:53:17+00:00

53b6f555a5068f3ded38c623f1939e082b3268ae












Intro pattern extensions for dup, swap and apply
2020-11-11T22:22:12+00:00

Cyril Cohen

2020-11-09T12:01:18+00:00

d84c26fa2eeeeb0029a56bac37bf1bae9f10882a












Turn class_of records into primitive records and get rid of the xclass idiom
2020-10-07T14:23:26+00:00

Kazuhiko Sakaguchi

2020-09-10T12:19:55+00:00

ad55cb4128382852370ea53d36f4d21a83274e8b












don't use all.v in output.v
2020-09-14T16:55:29+00:00

Enrico Tassi

2020-09-14T13:11:14+00:00

38b28c7d9756da7d346a1866a4ce712b1c3472af












fix 8.9, 8.8 and 8.7
2020-09-11T07:53:53+00:00

Enrico Tassi

2020-09-11T07:52:42+00:00

f3ad9538962cd36d90ea3a6724125f448d7c0b10












new attempt
2020-09-10T15:45:13+00:00

Enrico Tassi

2020-09-10T13:22:50+00:00

c7b1927d8072040d573757d543e2355e8280b9ee












default reference file for < 8.12
2020-09-09T13:22:29+00:00

Enrico Tassi

2020-09-09T13:22:29+00:00

c0214cdb4a44261db539b48fb76dbdaded87312b












[test suite] infrastructure to test how some statements are printed
2020-09-07T14:34:30+00:00

Enrico Tassi

2019-11-18T16:40:51+00:00

bc0a71056c24b29c8289395ee01740bb2ef7ad8d












Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition
2020-06-13T11:44:29+00:00

Kazuhiko Sakaguchi

2020-05-13T07:05:33+00:00

1e9eda65256af1f60547d067187d33f1d7cc1645