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--
Equality.v
584
log
plain
-rw-r--r--
Refine.v
583
log
plain
-rw-r--r--
auto.ml
29906
log
plain
-rw-r--r--
auto.mli
6259
log
plain
-rw-r--r--
autorewrite.ml
3309
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
812
log
plain
-rw-r--r--
contradiction.mli
734
log
plain
-rw-r--r--
dhyp.ml
10746
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--
elim.ml
5314
log
plain
-rw-r--r--
elim.mli
1335
log
plain
-rw-r--r--
eqdecide.ml4
5874
log
plain
-rw-r--r--
equality.ml
44084
log
plain
-rw-r--r--
equality.mli
2916
log
plain
-rw-r--r--
extraargs.ml4
1268
log
plain
-rw-r--r--
extraargs.mli
919
log
plain
-rw-r--r--
extratactics.ml4
7227
log
plain
-rw-r--r--
extratactics.mli
760
log
plain
-rw-r--r--
hiddentac.ml
4383
log
plain
-rw-r--r--
hiddentac.mli
3661
log
plain
-rw-r--r--
hipattern.ml
11595
log
plain
-rw-r--r--
hipattern.mli
4830
log
plain
-rw-r--r--
inv.ml
16333
log
plain
-rw-r--r--
inv.mli
1441
log
plain
-rw-r--r--
leminv.ml
10689
log
plain
-rw-r--r--
leminv.mli
440
log
plain
-rw-r--r--
nbtermdn.ml
2556
log
plain
-rw-r--r--
nbtermdn.mli
1328
log
plain
-rw-r--r--
refine.ml
10685
log
plain
-rw-r--r--
refine.mli
657
log
plain
-rw-r--r--
setoid_replace.ml
23778
log
plain
-rw-r--r--
setoid_replace.mli
942
log
plain
-rw-r--r--
tacinterp.ml
78389
log
plain
-rw-r--r--
tacinterp.mli
3985
log
plain
-rw-r--r--
tacticals.ml
14672
log
plain
-rw-r--r--
tacticals.mli
6144
log
plain
-rw-r--r--
tactics.ml
60802
log
plain
-rw-r--r--
tactics.mli
8902
log
plain
-rw-r--r--
tauto.ml4
6001
log
plain
-rw-r--r--
termdn.ml
2345
log
plain
-rw-r--r--
termdn.mli
1621
log
plain
-rw-r--r--
wcclausenv.ml
3168
log
plain
-rw-r--r--
wcclausenv.mli
1058
log
plain