index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
ssr
Mode
Name
Size
-rw-r--r--
absevarprop.v
3440
log
plain
-rw-r--r--
abstract_var2.v
969
log
plain
-rw-r--r--
binders.v
1887
log
plain
-rw-r--r--
binders_of.v
978
log
plain
-rw-r--r--
caseview.v
858
log
plain
-rw-r--r--
congr.v
1490
log
plain
-rw-r--r--
deferclear.v
1263
log
plain
-rw-r--r--
dependent_type_err.v
1060
log
plain
-rw-r--r--
derive_inversion.v
1140
log
plain
-rw-r--r--
elim.v
10179
log
plain
-rw-r--r--
elim2.v
2682
log
plain
-rw-r--r--
elim_pattern.v
1276
log
plain
-rw-r--r--
first_n.v
978
log
plain
-rw-r--r--
gen_have.v
5386
log
plain
-rw-r--r--
gen_pattern.v
1455
log
plain
-rw-r--r--
have_TC.v
1480
log
plain
-rw-r--r--
have_transp.v
1535
log
plain
-rw-r--r--
have_view_idiom.v
918
log
plain
-rw-r--r--
havesuff.v
2404
log
plain
-rw-r--r--
if_isnt.v
1004
log
plain
-rw-r--r--
intro_beta.v
1006
log
plain
-rw-r--r--
intro_noop.v
1434
log
plain
-rw-r--r--
ipatalternation.v
939
log
plain
-rw-r--r--
ltac_have.v
1372
log
plain
-rw-r--r--
ltac_in.v
1119
log
plain
-rw-r--r--
move_after.v
854
log
plain
-rw-r--r--
multiview.v
1987
log
plain
-rw-r--r--
occarrow.v
1111
log
plain
-rw-r--r--
patnoX.v
889
log
plain
-rw-r--r--
pattern.v
1190
log
plain
-rw-r--r--
primproj.v
3309
log
plain
-rw-r--r--
rewpatterns.v
5596
log
plain
-rw-r--r--
set_lamda.v
1131
log
plain
-rw-r--r--
set_pattern.v
3242
log
plain
-rw-r--r--
ssrsyntax2.v
905
log
plain
-rw-r--r--
tc.v
1471
log
plain
-rw-r--r--
typeof.v
912
log
plain
-rw-r--r--
unfold_Opaque.v
772
log
plain
-rw-r--r--
unkeyed.v
1281
log
plain
-rw-r--r--
view_case.v
1143
log
plain
-rw-r--r--
wlog_suff.v
1059
log
plain
-rw-r--r--
wlogletin.v
1811
log
plain
-rw-r--r--
wlong_intro.v
930
log
plain