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
1505
log
plain
-rw-r--r--
EAuto.v
3740
log
plain
-rw-r--r--
EqDecide.v
1595
log
plain
-rw-r--r--
Equality.v
5033
log
plain
-rw-r--r--
Inv.v
4641
log
plain
-rw-r--r--
Refine.v
721
log
plain
-rw-r--r--
Setoid_replace.v
1500
log
plain
-rw-r--r--
Tauto.v
774
log
plain
-rw-r--r--
auto.ml
30846
log
plain
-rw-r--r--
auto.mli
4970
log
plain
-rw-r--r--
autorewrite.ml
3964
log
plain
-rw-r--r--
autorewrite.mli
824
log
plain
-rw-r--r--
btermdn.ml
1521
log
plain
-rw-r--r--
btermdn.mli
893
log
plain
-rw-r--r--
dhyp.ml
9846
log
plain
-rw-r--r--
dhyp.mli
685
log
plain
-rw-r--r--
dn.ml
2915
log
plain
-rw-r--r--
dn.mli
1739
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml
10651
log
plain
-rw-r--r--
elim.ml
6668
log
plain
-rw-r--r--
elim.mli
1374
log
plain
-rw-r--r--
eqdecide.ml
6128
log
plain
-rw-r--r--
equality.ml
61370
log
plain
-rw-r--r--
equality.mli
4159
log
plain
-rw-r--r--
hiddentac.ml
1961
log
plain
-rw-r--r--
hiddentac.mli
1726
log
plain
-rw-r--r--
hipattern.ml
4930
log
plain
-rw-r--r--
hipattern.mli
2807
log
plain
-rw-r--r--
inv.ml
18709
log
plain
-rw-r--r--
inv.mli
1038
log
plain
-rw-r--r--
leminv.ml
13342
log
plain
-rw-r--r--
nbtermdn.ml
2556
log
plain
-rw-r--r--
nbtermdn.mli
1328
log
plain
-rw-r--r--
refine.ml
10974
log
plain
-rw-r--r--
refine.mli
651
log
plain
-rw-r--r--
setoid_replace.ml
23597
log
plain
-rw-r--r--
setoid_replace.mli
793
log
plain
-rw-r--r--
tacentries.ml
3142
log
plain
-rw-r--r--
tacentries.mli
2454
log
plain
-rw-r--r--
tacticals.ml
15632
log
plain
-rw-r--r--
tacticals.mli
5857
log
plain
-rw-r--r--
tactics.ml
65552
log
plain
-rw-r--r--
tactics.mli
10136
log
plain
-rw-r--r--
tauto.ml4
4690
log
plain
-rw-r--r--
termdn.ml
2331
log
plain
-rw-r--r--
termdn.mli
1621
log
plain
-rw-r--r--
wcclausenv.ml
5415
log
plain
-rw-r--r--
wcclausenv.mli
1396
log
plain