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
40844
log
plain
-rw-r--r--
auto.mli
7965
log
plain
-rw-r--r--
autorewrite.ml
10287
log
plain
-rw-r--r--
autorewrite.mli
1995
log
plain
-rw-r--r--
btermdn.ml
4579
log
plain
-rw-r--r--
btermdn.mli
1012
log
plain
-rw-r--r--
class_tactics.ml4
24909
log
plain
-rw-r--r--
contradiction.ml
2881
log
plain
-rw-r--r--
contradiction.mli
700
log
plain
-rw-r--r--
dhyp.ml
10857
log
plain
-rw-r--r--
dhyp.mli
1045
log
plain
-rw-r--r--
dn.ml
2449
log
plain
-rw-r--r--
dn.mli
1322
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml4
16403
log
plain
-rw-r--r--
eauto.mli
1294
log
plain
-rw-r--r--
elim.ml
5616
log
plain
-rw-r--r--
elim.mli
1361
log
plain
-rw-r--r--
elimschemes.ml
4897
log
plain
-rw-r--r--
elimschemes.mli
1311
log
plain
-rw-r--r--
eqdecide.ml4
6260
log
plain
-rw-r--r--
eqschemes.ml
30794
log
plain
-rw-r--r--
eqschemes.mli
1860
log
plain
-rw-r--r--
equality.ml
53448
log
plain
-rw-r--r--
equality.mli
5207
log
plain
-rw-r--r--
evar_tactics.ml
2167
log
plain
-rw-r--r--
evar_tactics.mli
797
log
plain
-rw-r--r--
extraargs.ml4
11679
log
plain
-rw-r--r--
extraargs.mli
2368
log
plain
-rw-r--r--
extratactics.ml4
16758
log
plain
-rw-r--r--
extratactics.mli
739
log
plain
-rw-r--r--
hiddentac.ml
5323
log
plain
-rw-r--r--
hiddentac.mli
4670
log
plain
-rw-r--r--
hightactics.mllib
73
log
plain
-rw-r--r--
hipattern.ml4
16212
log
plain
-rw-r--r--
hipattern.mli
6486
log
plain
-rw-r--r--
inv.ml
18554
log
plain
-rw-r--r--
inv.mli
1498
log
plain
-rw-r--r--
leminv.ml
10394
log
plain
-rw-r--r--
leminv.mli
544
log
plain
-rw-r--r--
nbtermdn.ml
4578
log
plain
-rw-r--r--
nbtermdn.mli
1490
log
plain
-rw-r--r--
refine.ml
12632
log
plain
-rw-r--r--
refine.mli
567
log
plain
-rw-r--r--
rewrite.ml4
66031
log
plain
-rw-r--r--
tacinterp.ml
117275
log
plain
-rw-r--r--
tacinterp.mli
5686
log
plain
-rw-r--r--
tactic_option.ml
2097
log
plain
-rw-r--r--
tactic_option.mli
754
log
plain
-rw-r--r--
tacticals.ml
16084
log
plain
-rw-r--r--
tacticals.mli
8509
log
plain
-rw-r--r--
tactics.ml
131732
log
plain
-rw-r--r--
tactics.mli
14529
log
plain
-rw-r--r--
tactics.mllib
196
log
plain
-rw-r--r--
tauto.ml4
9448
log
plain
-rw-r--r--
termdn.ml
4000
log
plain
-rw-r--r--
termdn.mli
2321
log
plain