index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
ssr
/
under.v
Age
Commit message (
Expand
)
Author
2019-12-27
fix: Shorten ssrsetoid.v
Erik Martin-Dorel
2019-11-01
[ssr] Refactor/Extend of under to support more relations
Erik Martin-Dorel
2019-09-10
[ssr] Add test "do [under ... do ...] in H"
Erik Martin-Dorel
2019-08-08
[ssr] under: Add a contrived example to test under/over with Setoids
Erik Martin-Dorel
2019-08-08
[ssr] Refactor under's Setoid generalization to ease stdlib2 porting
Erik Martin-Dorel
2019-08-06
[ssr] under: extend ssreflect.v to generalize iff to any setoid eq
Erik Martin-Dorel
2019-04-23
[ssr] set under's tactic argument at LEVEL 3
Erik Martin-Dorel
2019-04-23
[ssr] under: optimization of the tactic for (under eq_bigl => *)
Erik Martin-Dorel
2019-04-23
[ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc
Erik Martin-Dorel
2019-04-23
[ssr] under: Add iff support in side-conditions
Erik Martin-Dorel
2019-04-23
[ssr] new syntax for the under tactic
Enrico Tassi
2019-04-23
[ssr] under(one-liner version): Do nf_betaiota in the last goal
Erik Martin-Dorel
2019-04-23
[ssr] under: Change the style of a few tests (over tactic vs. lemma)
Erik Martin-Dorel
2019-04-23
[ssr] under: Add a fancy test with several kinds of side-conditions
Erik Martin-Dorel
2019-04-23
[ssr] under: Strenghten over & Add test_big_andb
Erik Martin-Dorel
2019-04-23
[ssr] under: Extend the test-suite to exemplify most use cases
Erik Martin-Dorel
2019-04-23
[ssr] Define both a lemma "over" (in sig UNDER) and an ltac "over"
Erik Martin-Dorel
2019-04-23
[ssr] under: Rename bound variables a posteriori for cosmetic purpose
Enrico Tassi
2019-04-02
[ssr] implement "under i: ext_lemma" by rewrite rule
Enrico Tassi
