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--
auto.ml
37883
log
plain
-rw-r--r--
auto.mli
7315
log
plain
-rw-r--r--
autorewrite.ml
7867
log
plain
-rw-r--r--
autorewrite.mli
1126
log
plain
-rw-r--r--
btermdn.ml
2583
log
plain
-rw-r--r--
btermdn.mli
997
log
plain
-rw-r--r--
class_tactics.ml4
71735
log
plain
-rw-r--r--
contradiction.ml
2896
log
plain
-rw-r--r--
contradiction.mli
739
log
plain
-rw-r--r--
decl_interp.ml
16858
log
plain
-rw-r--r--
decl_interp.mli
771
log
plain
-rw-r--r--
decl_proof_instr.ml
46338
log
plain
-rw-r--r--
decl_proof_instr.mli
3735
log
plain
-rw-r--r--
dhyp.ml
11502
log
plain
-rw-r--r--
dhyp.mli
1126
log
plain
-rw-r--r--
dn.ml
3485
log
plain
-rw-r--r--
dn.mli
1958
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml4
14363
log
plain
-rw-r--r--
eauto.mli
1095
log
plain
-rw-r--r--
elim.ml
5673
log
plain
-rw-r--r--
elim.mli
1399
log
plain
-rw-r--r--
eqdecide.ml4
6341
log
plain
-rw-r--r--
equality.ml
48874
log
plain
-rw-r--r--
equality.mli
5089
log
plain
-rw-r--r--
evar_tactics.ml
2483
log
plain
-rw-r--r--
evar_tactics.mli
800
log
plain
-rw-r--r--
extraargs.ml4
12300
log
plain
-rw-r--r--
extraargs.mli
2647
log
plain
-rw-r--r--
extratactics.ml4
18461
log
plain
-rw-r--r--
extratactics.mli
688
log
plain
-rw-r--r--
hiddentac.ml
6014
log
plain
-rw-r--r--
hiddentac.mli
4687
log
plain
-rw-r--r--
hipattern.ml4
11130
log
plain
-rw-r--r--
hipattern.mli
4757
log
plain
-rw-r--r--
inv.ml
19362
log
plain
-rw-r--r--
inv.mli
1537
log
plain
-rw-r--r--
leminv.ml
10627
log
plain
-rw-r--r--
leminv.mli
545
log
plain
-rw-r--r--
nbtermdn.ml
2649
log
plain
-rw-r--r--
nbtermdn.mli
1353
log
plain
-rw-r--r--
refine.ml
12323
log
plain
-rw-r--r--
refine.mli
593
log
plain
-rw-r--r--
setoid_replace.ml
78926
log
plain
-rw-r--r--
setoid_replace.mli
2922
log
plain
-rw-r--r--
tacinterp.ml
111296
log
plain
-rw-r--r--
tacinterp.mli
5439
log
plain
-rw-r--r--
tacticals.ml
15096
log
plain
-rw-r--r--
tacticals.mli
6908
log
plain
-rw-r--r--
tactics.ml
116415
log
plain
-rw-r--r--
tactics.mli
14070
log
plain
-rw-r--r--
tauto.ml4
5935
log
plain
-rw-r--r--
termdn.ml
2829
log
plain
-rw-r--r--
termdn.mli
2133
log
plain