| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-12-11 | Initial import of order.v into mathcomp | Cohen Cyril | |
| 2019-06-18 | Merge pull request #340 from pi8027/hierarchy | Enrico | |
| Reimplement the hierarchy related tools in OCaml | |||
| 2019-05-17 | refactor `seq` permutation theory | Georges Gonthier | |
| - Change the naming of permutation lemmas so they conform to a consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`) prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq` using a property when there is also a lemma _using_ `perm_eq` for the same property. Lemmas that do not concern `perm_eq` do _not_ have `perm` in their name. - Change the definition of `permutations` for a time- and space- back-to-front generation algorithm. - Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and `tally_seq`, used by the improved `permutation` algorithm. - add deprecated aliases for renamed lemmas | |||
| 2019-04-30 | Ad-hoc fix | Kazuhiko Sakaguchi | |
| 2019-04-03 | rename test-suite -> test_suite to make coq happy | Enrico Tassi | |
| 2019-04-02 | identifying missing joins | Cyril Cohen | |
| 2019-02-05 | we silence warnings that just pollute our logs (#275) | Enrico | |
| Namely: -projection-no-head-constant -redundant-canonical-projection -notation-overridden | |||
| 2018-10-26 | moving countalg and closed_field around | Cyril Cohen | |
| - countalg goes to the algebra package - finalg now get the expected inheritance from countalg - closed_field now contains the construction of algebraic closure for countable fields (previously in countalg) - proof of quantifier elimination for closed field rewritten in a monadic style | |||
| 2018-04-20 | Merge remote-tracking branch 'origin/pr/189' | Enrico Tassi | |
| 2018-04-20 | Merge remote-tracking branch 'origin/pr/192' | Enrico Tassi | |
| 2018-04-18 | Moving real_closed to another repo | Cyril Cohen | |
| 2018-04-17 | move odd_order to its own repository | Enrico Tassi | |
| 2018-04-12 | remove ssrtest: it now belongs to Coq | Enrico Tassi | |
| 2018-02-26 | Add ssrmatching.v transitional file | Erik Martin-Dorel | |
| The content of this file is similar to that of ssrfun.v and aims to increase compatibility with Coq 8.6+ for third-party libraries that depend on both math-comp and ssrmatching.v Close #63 | |||
| 2018-02-06 | add 3 tests to Make | Enrico Tassi | |
| 2017-06-07 | For trunk, use merged ssr plugin. | Maxime Dénès | |
| 2016-12-07 | new test for "rewrite /x" when x is Opaque | Enrico Tassi | |
| 2016-12-06 | add test for unfolding primitive projections | Enrico Tassi | |
| 2016-06-17 | this test is now in Coq, removing it. | Enrico Tassi | |
| 2016-06-16 | Port build system to trunk (ssrmatching merged in Coq) | Enrico Tassi | |
| 2016-02-25 | ssrpattern: compose nicely with Tactic Notation | Enrico Tassi | |
| 2015-12-04 | Move finfield to field module | Georges Gonthier | |
| 2015-11-05 | merge basic/ into ssreflect/ | Enrico Tassi | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |