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
4293
log
plain
-rw-r--r--
abstract.mli
1335
log
plain
-rw-r--r--
auto.ml
19822
log
plain
-rw-r--r--
auto.mli
3108
log
plain
-rw-r--r--
autorewrite.ml
10635
log
plain
-rw-r--r--
autorewrite.mli
2123
log
plain
-rw-r--r--
btermdn.ml
6286
log
plain
-rw-r--r--
btermdn.mli
1721
log
plain
-rw-r--r--
cbn.ml
31005
log
plain
-rw-r--r--
cbn.mli
784
log
plain
-rw-r--r--
class_tactics.ml
46739
log
plain
-rw-r--r--
class_tactics.mli
2497
log
plain
-rw-r--r--
contradiction.ml
5558
log
plain
-rw-r--r--
contradiction.mli
857
log
plain
-rw-r--r--
declareScheme.ml
1796
log
plain
-rw-r--r--
declareScheme.mli
865
log
plain
-rw-r--r--
declareUctx.ml
1572
log
plain
-rw-r--r--
declareUctx.mli
746
log
plain
-rw-r--r--
dn.ml
2544
log
plain
-rw-r--r--
dn.mli
1165
log
plain
-rw-r--r--
dnet.ml
10997
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
17402
log
plain
-rw-r--r--
eauto.mli
1501
log
plain
-rw-r--r--
elim.ml
9447
log
plain
-rw-r--r--
elim.mli
1233
log
plain
-rw-r--r--
elimschemes.ml
6671
log
plain
-rw-r--r--
elimschemes.mli
1891
log
plain
-rw-r--r--
eqdecide.ml
10122
log
plain
-rw-r--r--
eqdecide.mli
1159
log
plain
-rw-r--r--
eqschemes.ml
44470
log
plain
-rw-r--r--
eqschemes.mli
2205
log
plain
-rw-r--r--
equality.ml
76225
log
plain
-rw-r--r--
equality.mli
6581
log
plain
-rw-r--r--
genredexpr.ml
2549
log
plain
-rw-r--r--
hints.ml
60363
log
plain
-rw-r--r--
hints.mli
8905
log
plain
-rw-r--r--
hipattern.ml
21457
log
plain
-rw-r--r--
hipattern.mli
6861
log
plain
-rw-r--r--
ind_tables.ml
8253
log
plain
-rw-r--r--
ind_tables.mli
2809
log
plain
-rw-r--r--
inv.ml
21750
log
plain
-rw-r--r--
inv.mli
1412
log
plain
-rw-r--r--
ppred.ml
3251
log
plain
-rw-r--r--
ppred.mli
699
log
plain
-rw-r--r--
redexpr.ml
10195
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
30323
log
plain
-rw-r--r--
tacticals.mli
11591
log
plain
-rw-r--r--
tactics.ml
214039
log
plain
-rw-r--r--
tactics.mli
20911
log
plain
-rw-r--r--
tactics.mllib
242
log
plain
-rw-r--r--
term_dnet.ml
15637
log
plain
-rw-r--r--
term_dnet.mli
2796
log
plain