index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
ssr
Age
Commit message (
Expand
)
Author
2019-02-11
[ssr] keep user annotation on views (fix #9538)
Enrico Tassi
2019-01-19
[ssr] compile "=> {x..} y" as "=> {x..y} y"
Enrico Tassi
2019-01-18
[ssr] compile "=> {} y" as "=> {y} y"
Enrico Tassi
2018-12-18
[ssr] make > a stand alone intro pattern
Enrico Tassi
2018-12-18
[ssr] new test by Arthur Charguéraud
Enrico Tassi
2018-12-18
[ssr] extended intro patterns: + > [^] /ltac:
Enrico Tassi
2018-11-14
ssr: add another test for elim + TC
Enrico Tassi
2018-11-14
ssrmatching: unify_HO does not resolve type classes
Enrico Tassi
2018-09-19
[ssr] use the right environment in ssrpattern (fix #8454)
Enrico Tassi
2018-08-30
[ssr] move ssr_*v tests to test-suite/ssr/
Enrico Tassi
2018-06-25
Merge PR #7620: [ssr] rewrite: turn anomaly into regular error
Maxime Dénès
2018-06-23
Merge PR #7236: [ssr] simpler semantics for delayed clears
Maxime Dénès
2018-06-22
[ssr] implement {}/v as a short hand for {v}/v when v is an id
Enrico Tassi
2018-06-22
[ssr] test case for rewrite and set on univ poly keys
Enrico Tassi
2018-06-20
[ssr] test case for rewrite (setoid) making the goal illtyped
Enrico Tassi
2018-05-15
[ssr] import ssreflect test suite from math-comp
Enrico Tassi