aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Make
AgeCommit message (Expand)Author
2021-03-12Silencing warning deprecated-ident-entryCyril Cohen
2021-03-04Silence Hint Locality warningCyril Cohen
2020-11-19Removing duplicate clears and turning the warning into an errorCyril Cohen
2020-11-19add declare scopesReynald Affeldt
2020-10-07Turn class_of records into primitive records and get rid of the xclass idiomKazuhiko Sakaguchi
2020-04-06Rewriting with AC (not modulo AC), using a small scale command.Cyril Cohen
2019-12-11Initial import of order.v into mathcompCohen Cyril
2019-06-18Merge pull request #340 from pi8027/hierarchyEnrico
2019-05-17refactor `seq` permutation theoryGeorges Gonthier
2019-04-30Ad-hoc fixKazuhiko Sakaguchi
2019-04-03rename test-suite -> test_suite to make coq happyEnrico Tassi
2019-04-02identifying missing joinsCyril Cohen
2019-02-05we silence warnings that just pollute our logs (#275)Enrico
2018-10-26moving countalg and closed_field aroundCyril Cohen
2018-04-20Merge remote-tracking branch 'origin/pr/189'Enrico Tassi
2018-04-20Merge remote-tracking branch 'origin/pr/192'Enrico Tassi
2018-04-18Moving real_closed to another repoCyril Cohen
2018-04-17move odd_order to its own repositoryEnrico Tassi
2018-04-12remove ssrtest: it now belongs to CoqEnrico Tassi
2018-02-26Add ssrmatching.v transitional fileErik Martin-Dorel
2018-02-06add 3 tests to MakeEnrico Tassi
2017-06-07For trunk, use merged ssr plugin.Maxime Dénès
2016-12-07new test for "rewrite /x" when x is OpaqueEnrico Tassi
2016-12-06add test for unfolding primitive projectionsEnrico Tassi
2016-06-17this test is now in Coq, removing it.Enrico Tassi
2016-06-16Port build system to trunk (ssrmatching merged in Coq)Enrico Tassi
2016-02-25ssrpattern: compose nicely with Tactic NotationEnrico Tassi
2015-12-04Move finfield to field moduleGeorges Gonthier
2015-11-05merge basic/ into ssreflect/Enrico Tassi
2015-07-17Updating files + reorganizing everythingCyril Cohen
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:02:29 +0000