index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Mode
Name
Size
-rw-r--r--
Equality.v
7961
log
plain
-rw-r--r--
Tauto.v
251
log
plain
-rw-r--r--
auto.ml
29068
log
plain
-rw-r--r--
auto.mli
4181
log
plain
-rw-r--r--
btermdn.ml
1149
log
plain
-rw-r--r--
btermdn.mli
341
log
plain
-rw-r--r--
dhyp.ml
9283
log
plain
-rw-r--r--
dhyp.mli
165
log
plain
-rw-r--r--
dn.ml
2495
log
plain
-rw-r--r--
dn.mli
714
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
elim.ml
5316
log
plain
-rw-r--r--
elim.mli
961
log
plain
-rw-r--r--
equality.ml
68725
log
plain
-rw-r--r--
equality.mli
4037
log
plain
-rw-r--r--
hiddentac.ml
1414
log
plain
-rw-r--r--
hiddentac.mli
1207
log
plain
-rw-r--r--
nbtermdn.ml
2014
log
plain
-rw-r--r--
nbtermdn.mli
771
log
plain
-rw-r--r--
pattern.ml
9825
log
plain
-rw-r--r--
pattern.mli
4183
log
plain
-rw-r--r--
stock.ml
4088
log
plain
-rw-r--r--
stock.mli
387
log
plain
-rw-r--r--
tacentries.ml
2335
log
plain
-rw-r--r--
tacentries.mli
1668
log
plain
-rw-r--r--
tacticals.ml
14874
log
plain
-rw-r--r--
tacticals.mli
4944
log
plain
-rw-r--r--
tactics.ml
57513
log
plain
-rw-r--r--
tactics.mli
8378
log
plain
-rw-r--r--
tauto.ml
62448
log
plain
-rw-r--r--
tauto.mli
4488
log
plain
-rw-r--r--
termdn.ml
1557
log
plain
-rw-r--r--
termdn.mli
518
log
plain
-rw-r--r--
wcclausenv.ml
6757
log
plain
-rw-r--r--
wcclausenv.mli
1332
log
plain