index
:
coq-mathcomp
master
Library of mathematical components formalized in Coq
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
mathcomp
/
ssrtest
Age
Commit message (
Collapse
)
Author
2018-04-12
remove ssrtest: it now belongs to Coq
Enrico Tassi
2018-02-22
Change Implicit Arguments to Arguments in odd_order
Jasper Hugunin
2018-02-21
Merge pull request #177 from gares/fix/missing-ssrtest-in-Make
Cyril Cohen
add 3 tests to Make
2018-02-06
add 3 tests to Make
Enrico Tassi
2018-02-06
running semi-automated linting on the whole library
Cyril Cohen
2017-10-23
Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)
Cyril Cohen
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