| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-10 | fix building with make flags | Ralf Jung | |
| Fixes #139 | |||
| 2017-06-07 | Change failing test. | Maxime Dénès | |
| 2017-03-23 | ssrtest/elim.v: don't depend on Function | Enrico Tassi | |
| We inline the lemmas it generated, to ectly test the same thing as before. | |||
| 2016-12-07 | better test for primitive projections | Enrico Tassi | |
| 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-11-07 | update copyright banner | Assia Mahboubi | |
| 2016-06-17 | fix parsing (coq trunk goal selector/ltac:) | Enrico Tassi | |
| 2016-06-17 | this test is now in Coq, removing it. | Enrico Tassi | |
| 2016-02-25 | ssrpattern: compose nicely with Tactic Notation | Enrico Tassi | |
| 2015-12-03 | fix: autogen + abstract variables clash | Enrico Tassi | |
| 2015-12-03 | fix: elim/v handles eliminator from Derive Inversion (issue #2) | Enrico Tassi | |
| Also: - fix elim trying to saturate too much and not raising the expected exn - fix fill_occ_pattern when occ is {-}, it used to lose the instantiation obtained by matching the term | |||
| 2015-12-03 | Add commands to trace the matching algorithm | Enrico Tassi | |
| 2015-07-28 | update copyright banner | Enrico Tassi | |
| 2015-07-22 | next blind fix | Cyril Cohen | |
| 2015-07-22 | blind fix | Cyril Cohen | |
| 2015-07-18 | update to preserve backward compatibility with v8.4 | Cyril Cohen | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
| 2015-04-09 | Using the From X Require Y for v8.4 | Cyril Cohen | |
| 2015-04-08 | makefiles that are version dependent | Cyril Cohen | |
| 2015-03-09 | Initial commit | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |