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
19455
log
plain
-rw-r--r--
auto.mli
3501
log
plain
-rw-r--r--
autorewrite.ml
11245
log
plain
-rw-r--r--
autorewrite.mli
2171
log
plain
-rw-r--r--
btermdn.ml
5238
log
plain
-rw-r--r--
btermdn.mli
1559
log
plain
-rw-r--r--
class_tactics.ml
31485
log
plain
-rw-r--r--
class_tactics.mli
1151
log
plain
-rw-r--r--
contradiction.ml
4183
log
plain
-rw-r--r--
contradiction.mli
705
log
plain
-rw-r--r--
coretactics.ml4
5897
log
plain
-rw-r--r--
dn.ml
2513
log
plain
-rw-r--r--
dn.mli
1166
log
plain
-rw-r--r--
dnet.ml
10175
log
plain
-rw-r--r--
dnet.mli
4514
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml4
22345
log
plain
-rw-r--r--
eauto.mli
1212
log
plain
-rw-r--r--
elim.ml
5562
log
plain
-rw-r--r--
elim.mli
1035
log
plain
-rw-r--r--
elimschemes.ml
6008
log
plain
-rw-r--r--
elimschemes.mli
1378
log
plain
-rw-r--r--
eqdecide.ml
7565
log
plain
-rw-r--r--
eqdecide.mli
1007
log
plain
-rw-r--r--
eqschemes.ml
41001
log
plain
-rw-r--r--
eqschemes.mli
2129
log
plain
-rw-r--r--
equality.ml
69119
log
plain
-rw-r--r--
equality.mli
5398
log
plain
-rw-r--r--
evar_tactics.ml
2978
log
plain
-rw-r--r--
evar_tactics.mli
883
log
plain
-rw-r--r--
extraargs.ml4
9512
log
plain
-rw-r--r--
extraargs.mli
2102
log
plain
-rw-r--r--
extratactics.ml4
35275
log
plain
-rw-r--r--
extratactics.mli
810
log
plain
-rw-r--r--
ftactic.ml
3011
log
plain
-rw-r--r--
ftactic.mli
2621
log
plain
-rw-r--r--
g_auto.ml4
2285
log
plain
-rw-r--r--
g_class.ml4
2694
log
plain
-rw-r--r--
g_eqdecide.ml4
1158
log
plain
-rw-r--r--
g_rewrite.ml4
12311
log
plain
-rw-r--r--
geninterp.ml
1177
log
plain
-rw-r--r--
geninterp.mli
1000
log
plain
-rw-r--r--
hightactics.mllib
114
log
plain
-rw-r--r--
hints.ml
47465
log
plain
-rw-r--r--
hints.mli
8243
log
plain
-rw-r--r--
hipattern.ml4
17695
log
plain
-rw-r--r--
hipattern.mli
6647
log
plain
-rw-r--r--
inv.ml
19906
log
plain
-rw-r--r--
inv.mli
1189
log
plain
-rw-r--r--
leminv.ml
9932
log
plain
-rw-r--r--
leminv.mli
792
log
plain
-rw-r--r--
rewrite.ml
80394
log
plain
-rw-r--r--
rewrite.mli
3403
log
plain
-rw-r--r--
taccoerce.ml
9966
log
plain
-rw-r--r--
taccoerce.mli
3172
log
plain
-rw-r--r--
tacenv.ml
4336
log
plain
-rw-r--r--
tacenv.mli
2690
log
plain
-rw-r--r--
tacintern.ml
32427
log
plain
-rw-r--r--
tacintern.mli
2025
log
plain
-rw-r--r--
tacinterp.ml
86466
log
plain
-rw-r--r--
tacinterp.mli
4296
log
plain
-rw-r--r--
tacsubst.ml
13152
log
plain
-rw-r--r--
tacsubst.mli
1108
log
plain
-rw-r--r--
tactic_matching.ml
14890
log
plain
-rw-r--r--
tactic_matching.mli
2205
log
plain
-rw-r--r--
tactic_option.ml
1962
log
plain
-rw-r--r--
tactic_option.mli
790
log
plain
-rw-r--r--
tacticals.ml
24310
log
plain
-rw-r--r--
tacticals.mli
12239
log
plain
-rw-r--r--
tactics.ml
186112
log
plain
-rw-r--r--
tactics.mli
18140
log
plain
-rw-r--r--
tactics.mllib
256
log
plain
-rw-r--r--
tauto.ml4
14811
log
plain
-rw-r--r--
term_dnet.ml
12742
log
plain
-rw-r--r--
term_dnet.mli
2640
log
plain