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
21139
log
plain
-rw-r--r--
auto.mli
3252
log
plain
-rw-r--r--
autorewrite.ml
11491
log
plain
-rw-r--r--
autorewrite.mli
2429
log
plain
-rw-r--r--
btermdn.ml
5776
log
plain
-rw-r--r--
btermdn.mli
1716
log
plain
-rw-r--r--
cbn.ml
30771
log
plain
-rw-r--r--
cbn.mli
784
log
plain
-rw-r--r--
class_tactics.ml
48688
log
plain
-rw-r--r--
class_tactics.mli
2657
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
17757
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
44069
log
plain
-rw-r--r--
eqschemes.mli
2205
log
plain
-rw-r--r--
equality.ml
76075
log
plain
-rw-r--r--
equality.mli
6748
log
plain
-rw-r--r--
genredexpr.ml
2549
log
plain
-rw-r--r--
hints.ml
56958
log
plain
-rw-r--r--
hints.mli
9429
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
9760
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
27249
log
plain
-rw-r--r--
tacticals.mli
12248
log
plain
-rw-r--r--
tactics.ml
213247
log
plain
-rw-r--r--
tactics.mli
20504
log
plain
-rw-r--r--
tactics.mllib
242
log
plain
-rw-r--r--
term_dnet.ml
14754
log
plain
-rw-r--r--
term_dnet.mli
2796
log
plain