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--
EAuto.v
2867
log
plain
-rw-r--r--
Equality.v
8032
log
plain
-rw-r--r--
Inv.v
3642
log
plain
-rw-r--r--
Refine.v
182
log
plain
-rw-r--r--
Tauto.v
256
log
plain
-rw-r--r--
auto.ml
29394
log
plain
-rw-r--r--
auto.mli
4285
log
plain
-rw-r--r--
btermdn.ml
1003
log
plain
-rw-r--r--
btermdn.mli
392
log
plain
-rw-r--r--
dhyp.ml
9309
log
plain
-rw-r--r--
dhyp.mli
165
log
plain
-rw-r--r--
dn.ml
2397
log
plain
-rw-r--r--
dn.mli
1219
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml
8444
log
plain
-rw-r--r--
elim.ml
5934
log
plain
-rw-r--r--
elim.mli
960
log
plain
-rw-r--r--
equality.ml
67669
log
plain
-rw-r--r--
equality.mli
4078
log
plain
-rw-r--r--
hiddentac.ml
1413
log
plain
-rw-r--r--
hiddentac.mli
1206
log
plain
-rw-r--r--
hipattern.ml
6317
log
plain
-rw-r--r--
hipattern.mli
5909
log
plain
-rw-r--r--
inv.ml
17600
log
plain
-rw-r--r--
inv.mli
510
log
plain
-rw-r--r--
leminv.ml
12310
log
plain
-rw-r--r--
nbtermdn.ml
2057
log
plain
-rw-r--r--
nbtermdn.mli
827
log
plain
-rw-r--r--
refine.ml
9242
log
plain
-rw-r--r--
refine.mli
101
log
plain
-rw-r--r--
tacentries.ml
2339
log
plain
-rw-r--r--
tacentries.mli
1675
log
plain
-rw-r--r--
tacticals.ml
14344
log
plain
-rw-r--r--
tacticals.mli
4976
log
plain
-rw-r--r--
tactics.ml
57463
log
plain
-rw-r--r--
tactics.mli
8366
log
plain
-rw-r--r--
tauto.ml
63412
log
plain
-rw-r--r--
tauto.mli
4488
log
plain
-rw-r--r--
termdn.ml
1777
log
plain
-rw-r--r--
termdn.mli
1120
log
plain
-rw-r--r--
wcclausenv.ml
6437
log
plain
-rw-r--r--
wcclausenv.mli
1434
log
plain