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
4201
log
plain
-rw-r--r--
abstract.mli
1335
log
plain
-rw-r--r--
auto.ml
21041
log
plain
-rw-r--r--
auto.mli
3193
log
plain
-rw-r--r--
autorewrite.ml
10635
log
plain
-rw-r--r--
autorewrite.mli
2123
log
plain
-rw-r--r--
btermdn.ml
5887
log
plain
-rw-r--r--
btermdn.mli
1716
log
plain
-rw-r--r--
cbn.ml
30864
log
plain
-rw-r--r--
cbn.mli
784
log
plain
-rw-r--r--
class_tactics.ml
48171
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
2758
log
plain
-rw-r--r--
dn.mli
1166
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
17498
log
plain
-rw-r--r--
eauto.mli
1466
log
plain
-rw-r--r--
elim.ml
5655
log
plain
-rw-r--r--
elim.mli
1201
log
plain
-rw-r--r--
elimschemes.ml
6671
log
plain
-rw-r--r--
elimschemes.mli
1891
log
plain
-rw-r--r--
eqdecide.ml
10106
log
plain
-rw-r--r--
eqdecide.mli
1159
log
plain
-rw-r--r--
eqschemes.ml
44226
log
plain
-rw-r--r--
eqschemes.mli
2205
log
plain
-rw-r--r--
equality.ml
76073
log
plain
-rw-r--r--
equality.mli
6748
log
plain
-rw-r--r--
genredexpr.ml
2549
log
plain
-rw-r--r--
hints.ml
57327
log
plain
-rw-r--r--
hints.mli
8776
log
plain
-rw-r--r--
hipattern.ml
21457
log
plain
-rw-r--r--
hipattern.mli
6861
log
plain
-rw-r--r--
ind_tables.ml
8250
log
plain
-rw-r--r--
ind_tables.mli
2809
log
plain
-rw-r--r--
inv.ml
21554
log
plain
-rw-r--r--
inv.mli
1412
log
plain
-rw-r--r--
ppred.ml
3251
log
plain
-rw-r--r--
ppred.mli
512
log
plain
-rw-r--r--
redexpr.ml
10193
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
33911
log
plain
-rw-r--r--
tacticals.mli
12369
log
plain
-rw-r--r--
tactics.ml
213630
log
plain
-rw-r--r--
tactics.mli
20504
log
plain
-rw-r--r--
tactics.mllib
242
log
plain
-rw-r--r--
term_dnet.ml
14758
log
plain
-rw-r--r--
term_dnet.mli
2796
log
plain