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
18397
log
plain
-rw-r--r--
auto.mli
3329
log
plain
-rw-r--r--
autorewrite.ml
10975
log
plain
-rw-r--r--
autorewrite.mli
2171
log
plain
-rw-r--r--
btermdn.ml
5240
log
plain
-rw-r--r--
btermdn.mli
1569
log
plain
-rw-r--r--
class_tactics.ml
27045
log
plain
-rw-r--r--
class_tactics.mli
1151
log
plain
-rw-r--r--
contradiction.ml
4062
log
plain
-rw-r--r--
contradiction.mli
705
log
plain
-rw-r--r--
coretactics.ml4
6333
log
plain
-rw-r--r--
dn.ml
2517
log
plain
-rw-r--r--
dn.mli
1175
log
plain
-rw-r--r--
dnet.ml
9767
log
plain
-rw-r--r--
dnet.mli
4470
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml4
21806
log
plain
-rw-r--r--
eauto.mli
1280
log
plain
-rw-r--r--
elim.ml
5516
log
plain
-rw-r--r--
elim.mli
1035
log
plain
-rw-r--r--
elimschemes.ml
5743
log
plain
-rw-r--r--
elimschemes.mli
1378
log
plain
-rw-r--r--
eqdecide.ml
7083
log
plain
-rw-r--r--
eqdecide.mli
1007
log
plain
-rw-r--r--
eqschemes.ml
40779
log
plain
-rw-r--r--
eqschemes.mli
2117
log
plain
-rw-r--r--
equality.ml
66168
log
plain
-rw-r--r--
equality.mli
5410
log
plain
-rw-r--r--
evar_tactics.ml
2853
log
plain
-rw-r--r--
evar_tactics.mli
896
log
plain
-rw-r--r--
extraargs.ml4
9512
log
plain
-rw-r--r--
extraargs.mli
2102
log
plain
-rw-r--r--
extratactics.ml4
34523
log
plain
-rw-r--r--
extratactics.mli
799
log
plain
-rw-r--r--
ftactic.ml
2916
log
plain
-rw-r--r--
ftactic.mli
2375
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
1188
log
plain
-rw-r--r--
geninterp.mli
1067
log
plain
-rw-r--r--
hightactics.mllib
107
log
plain
-rw-r--r--
hints.ml
43292
log
plain
-rw-r--r--
hints.mli
7926
log
plain
-rw-r--r--
hipattern.ml4
17687
log
plain
-rw-r--r--
hipattern.mli
6667
log
plain
-rw-r--r--
inv.ml
19683
log
plain
-rw-r--r--
inv.mli
1198
log
plain
-rw-r--r--
leminv.ml
9724
log
plain
-rw-r--r--
leminv.mli
801
log
plain
-rw-r--r--
rewrite.ml
79380
log
plain
-rw-r--r--
rewrite.mli
3570
log
plain
-rw-r--r--
taccoerce.ml
9134
log
plain
-rw-r--r--
taccoerce.mli
3116
log
plain
-rw-r--r--
tacenv.ml
3900
log
plain
-rw-r--r--
tacenv.mli
2169
log
plain
-rw-r--r--
tacintern.ml
32958
log
plain
-rw-r--r--
tacintern.mli
2065
log
plain
-rw-r--r--
tacinterp.ml
93674
log
plain
-rw-r--r--
tacinterp.mli
4603
log
plain
-rw-r--r--
tacsubst.ml
14537
log
plain
-rw-r--r--
tacsubst.mli
1108
log
plain
-rw-r--r--
tacticMatching.ml
14883
log
plain
-rw-r--r--
tacticMatching.mli
2146
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
23534
log
plain
-rw-r--r--
tacticals.mli
12161
log
plain
-rw-r--r--
tactics.ml
175639
log
plain
-rw-r--r--
tactics.mli
18078
log
plain
-rw-r--r--
tactics.mllib
255
log
plain
-rw-r--r--
tauto.ml4
13084
log
plain
-rw-r--r--
term_dnet.ml
12383
log
plain
-rw-r--r--
term_dnet.mli
2610
log
plain