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
57392
log
plain
-rw-r--r--
auto.mli
9748
log
plain
-rw-r--r--
autorewrite.ml
10957
log
plain
-rw-r--r--
autorewrite.mli
2171
log
plain
-rw-r--r--
btermdn.ml
5144
log
plain
-rw-r--r--
btermdn.mli
1569
log
plain
-rw-r--r--
class_tactics.ml
26712
log
plain
-rw-r--r--
class_tactics.mli
1149
log
plain
-rw-r--r--
contradiction.ml
4095
log
plain
-rw-r--r--
contradiction.mli
705
log
plain
-rw-r--r--
coretactics.ml4
3753
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
21508
log
plain
-rw-r--r--
eauto.mli
1274
log
plain
-rw-r--r--
elim.ml
5534
log
plain
-rw-r--r--
elim.mli
1048
log
plain
-rw-r--r--
elimschemes.ml
5784
log
plain
-rw-r--r--
elimschemes.mli
1378
log
plain
-rw-r--r--
eqdecide.ml
7062
log
plain
-rw-r--r--
eqdecide.mli
1007
log
plain
-rw-r--r--
eqschemes.ml
40990
log
plain
-rw-r--r--
eqschemes.mli
2117
log
plain
-rw-r--r--
equality.ml
66216
log
plain
-rw-r--r--
equality.mli
5504
log
plain
-rw-r--r--
evar_tactics.ml
2217
log
plain
-rw-r--r--
evar_tactics.mli
784
log
plain
-rw-r--r--
extraargs.ml4
9804
log
plain
-rw-r--r--
extraargs.mli
2096
log
plain
-rw-r--r--
extratactics.ml4
32570
log
plain
-rw-r--r--
extratactics.mli
799
log
plain
-rw-r--r--
g_class.ml4
2693
log
plain
-rw-r--r--
g_eqdecide.ml4
1158
log
plain
-rw-r--r--
g_rewrite.ml4
13254
log
plain
-rw-r--r--
geninterp.ml
1195
log
plain
-rw-r--r--
geninterp.mli
1067
log
plain
-rw-r--r--
hightactics.mllib
107
log
plain
-rw-r--r--
hipattern.ml4
17225
log
plain
-rw-r--r--
hipattern.mli
6652
log
plain
-rw-r--r--
inv.ml
19545
log
plain
-rw-r--r--
inv.mli
1216
log
plain
-rw-r--r--
leminv.ml
9674
log
plain
-rw-r--r--
leminv.mli
801
log
plain
-rw-r--r--
rewrite.ml
78708
log
plain
-rw-r--r--
rewrite.mli
3504
log
plain
-rw-r--r--
taccoerce.ml
8911
log
plain
-rw-r--r--
taccoerce.mli
2944
log
plain
-rw-r--r--
tacenv.ml
7962
log
plain
-rw-r--r--
tacenv.mli
2003
log
plain
-rw-r--r--
tacintern.ml
31455
log
plain
-rw-r--r--
tacintern.mli
2258
log
plain
-rw-r--r--
tacinterp.ml
80837
log
plain
-rw-r--r--
tacinterp.mli
4510
log
plain
-rw-r--r--
tacsubst.ml
13880
log
plain
-rw-r--r--
tacsubst.mli
1108
log
plain
-rw-r--r--
tacticMatching.ml
14718
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
21636
log
plain
-rw-r--r--
tacticals.mli
11787
log
plain
-rw-r--r--
tactics.ml
151068
log
plain
-rw-r--r--
tactics.mli
15966
log
plain
-rw-r--r--
tactics.mllib
241
log
plain
-rw-r--r--
tauto.ml4
12382
log
plain
-rw-r--r--
term_dnet.ml
12361
log
plain
-rw-r--r--
term_dnet.mli
2610
log
plain