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--
.cvsignore
9
log
plain
-rw-r--r--
AutoRewrite.v
987
log
plain
-rw-r--r--
EAuto.v
2915
log
plain
-rw-r--r--
EqDecide.v
1077
log
plain
-rw-r--r--
Equality.v
4494
log
plain
-rw-r--r--
Inv.v
3665
log
plain
-rw-r--r--
Refine.v
202
log
plain
-rw-r--r--
Tauto.v
256
log
plain
-rw-r--r--
auto.ml
30845
log
plain
-rw-r--r--
auto.mli
4402
log
plain
-rw-r--r--
autorewrite.ml
3421
log
plain
-rw-r--r--
autorewrite.mli
306
log
plain
-rw-r--r--
btermdn.ml
1003
log
plain
-rw-r--r--
btermdn.mli
375
log
plain
-rw-r--r--
dhyp.ml
9307
log
plain
-rw-r--r--
dhyp.mli
167
log
plain
-rw-r--r--
dn.ml
2397
log
plain
-rw-r--r--
dn.mli
1221
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml
8444
log
plain
-rw-r--r--
elim.ml
5931
log
plain
-rw-r--r--
elim.mli
962
log
plain
-rw-r--r--
eqdecide.ml
5535
log
plain
-rw-r--r--
equality.ml
63535
log
plain
-rw-r--r--
equality.mli
3724
log
plain
-rw-r--r--
hiddentac.ml
1413
log
plain
-rw-r--r--
hiddentac.mli
1208
log
plain
-rw-r--r--
hipattern.ml
4177
log
plain
-rw-r--r--
hipattern.mli
2234
log
plain
-rw-r--r--
inv.ml
18235
log
plain
-rw-r--r--
inv.mli
516
log
plain
-rw-r--r--
leminv.ml
12567
log
plain
-rw-r--r--
nbtermdn.ml
2038
log
plain
-rw-r--r--
nbtermdn.mli
810
log
plain
-rw-r--r--
refine.ml
8810
log
plain
-rw-r--r--
refine.mli
147
log
plain
-rw-r--r--
tacentries.ml
2285
log
plain
-rw-r--r--
tacentries.mli
1677
log
plain
-rw-r--r--
tacticals.ml
14375
log
plain
-rw-r--r--
tacticals.mli
5054
log
plain
-rw-r--r--
tactics.ml
59776
log
plain
-rw-r--r--
tactics.mli
8677
log
plain
-rw-r--r--
tauto.ml4
4021
log
plain
-rw-r--r--
termdn.ml
1824
log
plain
-rw-r--r--
termdn.mli
1103
log
plain
-rw-r--r--
wcclausenv.ml
6345
log
plain
-rw-r--r--
wcclausenv.mli
1416
log
plain