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
52329
log
plain
-rw-r--r--
auto.mli
9333
log
plain
-rw-r--r--
autorewrite.ml
10502
log
plain
-rw-r--r--
autorewrite.mli
2115
log
plain
-rw-r--r--
btermdn.ml
4611
log
plain
-rw-r--r--
btermdn.mli
1024
log
plain
-rw-r--r--
class_tactics.ml
26333
log
plain
-rw-r--r--
class_tactics.mli
1149
log
plain
-rw-r--r--
contradiction.ml
3982
log
plain
-rw-r--r--
contradiction.mli
732
log
plain
-rw-r--r--
dn.ml
2501
log
plain
-rw-r--r--
dn.mli
1322
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml4
19643
log
plain
-rw-r--r--
eauto.mli
1328
log
plain
-rw-r--r--
elim.ml
6030
log
plain
-rw-r--r--
elim.mli
1545
log
plain
-rw-r--r--
elimschemes.ml
4584
log
plain
-rw-r--r--
elimschemes.mli
1378
log
plain
-rw-r--r--
eqdecide.ml4
7695
log
plain
-rw-r--r--
eqschemes.ml
38364
log
plain
-rw-r--r--
eqschemes.mli
1878
log
plain
-rw-r--r--
equality.ml
64243
log
plain
-rw-r--r--
equality.mli
6016
log
plain
-rw-r--r--
evar_tactics.ml
2251
log
plain
-rw-r--r--
evar_tactics.mli
765
log
plain
-rw-r--r--
extraargs.ml4
11931
log
plain
-rw-r--r--
extraargs.mli
2464
log
plain
-rw-r--r--
extratactics.ml4
29369
log
plain
-rw-r--r--
extratactics.mli
810
log
plain
-rw-r--r--
g_class.ml4
2682
log
plain
-rw-r--r--
g_rewrite.ml4
13245
log
plain
-rw-r--r--
geninterp.ml
1190
log
plain
-rw-r--r--
geninterp.mli
1067
log
plain
-rw-r--r--
hiddentac.ml
3335
log
plain
-rw-r--r--
hiddentac.mli
5208
log
plain
-rw-r--r--
hightactics.mllib
84
log
plain
-rw-r--r--
hipattern.ml4
17448
log
plain
-rw-r--r--
hipattern.mli
6573
log
plain
-rw-r--r--
inv.ml
20887
log
plain
-rw-r--r--
inv.mli
1639
log
plain
-rw-r--r--
leminv.ml
10267
log
plain
-rw-r--r--
leminv.mli
1130
log
plain
-rw-r--r--
rewrite.ml
72651
log
plain
-rw-r--r--
rewrite.mli
2922
log
plain
-rw-r--r--
taccoerce.ml
8479
log
plain
-rw-r--r--
taccoerce.mli
2772
log
plain
-rw-r--r--
tacintern.ml
37001
log
plain
-rw-r--r--
tacintern.mli
2509
log
plain
-rw-r--r--
tacinterp.ml
93186
log
plain
-rw-r--r--
tacinterp.mli
4348
log
plain
-rw-r--r--
tacsubst.ml
14140
log
plain
-rw-r--r--
tacsubst.mli
1108
log
plain
-rw-r--r--
tactic_option.ml
1962
log
plain
-rw-r--r--
tactic_option.mli
806
log
plain
-rw-r--r--
tacticals.ml
23299
log
plain
-rw-r--r--
tacticals.mli
11962
log
plain
-rw-r--r--
tactics.ml
149542
log
plain
-rw-r--r--
tactics.mli
16518
log
plain
-rw-r--r--
tactics.mllib
221
log
plain
-rw-r--r--
tauto.ml4
12363
log
plain
-rw-r--r--
termdn.ml
3994
log
plain
-rw-r--r--
termdn.mli
2334
log
plain