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
19836
log
plain
-rw-r--r--
auto.mli
3108
log
plain
-rw-r--r--
autorewrite.ml
11133
log
plain
-rw-r--r--
autorewrite.mli
2160
log
plain
-rw-r--r--
btermdn.ml
6286
log
plain
-rw-r--r--
btermdn.mli
1721
log
plain
-rw-r--r--
cbn.ml
31409
log
plain
-rw-r--r--
cbn.mli
1073
log
plain
-rw-r--r--
class_tactics.ml
46813
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
1591
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
150
log
plain
-rw-r--r--
eauto.ml
17423
log
plain
-rw-r--r--
eauto.mli
1501
log
plain
-rw-r--r--
elim.ml
7728
log
plain
-rw-r--r--
elim.mli
1137
log
plain
-rw-r--r--
elimschemes.ml
6671
log
plain
-rw-r--r--
elimschemes.mli
1891
log
plain
-rw-r--r--
eqdecide.ml
10144
log
plain
-rw-r--r--
eqdecide.mli
1159
log
plain
-rw-r--r--
eqschemes.ml
44686
log
plain
-rw-r--r--
eqschemes.mli
2205
log
plain
-rw-r--r--
equality.ml
76688
log
plain
-rw-r--r--
equality.mli
6774
log
plain
-rw-r--r--
genredexpr.ml
2606
log
plain
-rw-r--r--
hints.ml
61160
log
plain
-rw-r--r--
hints.mli
8986
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
12831
log
plain
-rw-r--r--
redexpr.mli
2164
log
plain
-rw-r--r--
redops.ml
2693
log
plain
-rw-r--r--
redops.mli
934
log
plain
-rw-r--r--
tacticals.ml
31304
log
plain
-rw-r--r--
tacticals.mli
11877
log
plain
-rw-r--r--
tactics.ml
210565
log
plain
-rw-r--r--
tactics.mli
20474
log
plain
-rw-r--r--
tactics.mllib
242
log
plain
-rw-r--r--
term_dnet.ml
15673
log
plain
-rw-r--r--
term_dnet.mli
2796
log
plain