index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
Mode
Name
Size
-rw-r--r--
abstract.ml
7828
log
plain
-rw-r--r--
abstract.mli
1312
log
plain
-rw-r--r--
auto.ml
20416
log
plain
-rw-r--r--
auto.mli
3252
log
plain
-rw-r--r--
autorewrite.ml
11005
log
plain
-rw-r--r--
autorewrite.mli
2359
log
plain
-rw-r--r--
btermdn.ml
5686
log
plain
-rw-r--r--
btermdn.mli
1716
log
plain
-rw-r--r--
class_tactics.ml
46831
log
plain
-rw-r--r--
class_tactics.mli
2490
log
plain
-rw-r--r--
contradiction.ml
5305
log
plain
-rw-r--r--
contradiction.mli
857
log
plain
-rw-r--r--
declare.ml
25466
log
plain
-rw-r--r--
declare.mli
3962
log
plain
-rw-r--r--
dn.ml
2513
log
plain
-rw-r--r--
dn.mli
1166
log
plain
-rw-r--r--
dnet.ml
10325
log
plain
-rw-r--r--
dnet.mli
4665
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
dune
145
log
plain
-rw-r--r--
eauto.ml
18117
log
plain
-rw-r--r--
eauto.mli
1537
log
plain
-rw-r--r--
elim.ml
5638
log
plain
-rw-r--r--
elim.mli
1201
log
plain
-rw-r--r--
elimschemes.ml
6788
log
plain
-rw-r--r--
elimschemes.mli
2081
log
plain
-rw-r--r--
eqdecide.ml
9972
log
plain
-rw-r--r--
eqdecide.mli
1159
log
plain
-rw-r--r--
eqschemes.ml
43635
log
plain
-rw-r--r--
eqschemes.mli
2247
log
plain
-rw-r--r--
equality.ml
74314
log
plain
-rw-r--r--
equality.mli
6675
log
plain
-rw-r--r--
genredexpr.ml
2549
log
plain
-rw-r--r--
hints.ml
60057
log
plain
-rw-r--r--
hints.mli
11008
log
plain
-rw-r--r--
hipattern.ml
21217
log
plain
-rw-r--r--
hipattern.mli
6849
log
plain
-rw-r--r--
ind_tables.ml
7530
log
plain
-rw-r--r--
ind_tables.mli
2281
log
plain
-rw-r--r--
inv.ml
21268
log
plain
-rw-r--r--
inv.mli
1412
log
plain
-rw-r--r--
leminv.ml
10750
log
plain
-rw-r--r--
leminv.mli
960
log
plain
-rw-r--r--
ppred.ml
3251
log
plain
-rw-r--r--
ppred.mli
512
log
plain
-rw-r--r--
redexpr.ml
10087
log
plain
-rw-r--r--
redexpr.mli
1886
log
plain
-rw-r--r--
redops.ml
2693
log
plain
-rw-r--r--
redops.mli
934
log
plain
-rw-r--r--
tacticals.ml
26398
log
plain
-rw-r--r--
tacticals.mli
12077
log
plain
-rw-r--r--
tactics.ml
202953
log
plain
-rw-r--r--
tactics.mli
20125
log
plain
-rw-r--r--
tactics.mllib
227
log
plain
-rw-r--r--
term_dnet.ml
14164
log
plain
-rw-r--r--
term_dnet.mli
2796
log
plain