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--
auto.ml
30451
log
plain
-rw-r--r--
auto.mli
6259
log
plain
-rw-r--r--
autorewrite.ml
3435
log
plain
-rw-r--r--
autorewrite.mli
851
log
plain
-rw-r--r--
btermdn.ml
1521
log
plain
-rw-r--r--
btermdn.mli
893
log
plain
-rw-r--r--
contradiction.ml
2659
log
plain
-rw-r--r--
contradiction.mli
719
log
plain
-rw-r--r--
dhyp.ml
10784
log
plain
-rw-r--r--
dhyp.mli
1119
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.ml4
12429
log
plain
-rw-r--r--
eauto.mli
840
log
plain
-rw-r--r--
elim.ml
5612
log
plain
-rw-r--r--
elim.mli
1375
log
plain
-rw-r--r--
eqdecide.ml4
5874
log
plain
-rw-r--r--
equality.ml
44229
log
plain
-rw-r--r--
equality.mli
2900
log
plain
-rw-r--r--
extraargs.ml4
1268
log
plain
-rw-r--r--
extraargs.mli
919
log
plain
-rw-r--r--
extratactics.ml4
6329
log
plain
-rw-r--r--
extratactics.mli
760
log
plain
-rw-r--r--
hiddentac.ml
4405
log
plain
-rw-r--r--
hiddentac.mli
3667
log
plain
-rw-r--r--
hipattern.ml
11595
log
plain
-rw-r--r--
hipattern.mli
4830
log
plain
-rw-r--r--
inv.ml
19381
log
plain
-rw-r--r--
inv.mli
1458
log
plain
-rw-r--r--
leminv.ml
10510
log
plain
-rw-r--r--
leminv.mli
528
log
plain
-rw-r--r--
nbtermdn.ml
2556
log
plain
-rw-r--r--
nbtermdn.mli
1328
log
plain
-rw-r--r--
refine.ml
10690
log
plain
-rw-r--r--
refine.mli
657
log
plain
-rw-r--r--
setoid_replace.ml
23862
log
plain
-rw-r--r--
setoid_replace.mli
942
log
plain
-rw-r--r--
tacinterp.ml
79517
log
plain
-rw-r--r--
tacinterp.mli
4058
log
plain
-rw-r--r--
tacticals.ml
14415
log
plain
-rw-r--r--
tacticals.mli
6122
log
plain
-rw-r--r--
tactics.ml
60188
log
plain
-rw-r--r--
tactics.mli
8835
log
plain
-rw-r--r--
tauto.ml4
6126
log
plain
-rw-r--r--
termdn.ml
2345
log
plain
-rw-r--r--
termdn.mli
1621
log
plain