index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Mode
Name
Size
-rw-r--r--
auto.ml
40838
log
plain
-rw-r--r--
auto.mli
7914
log
plain
-rw-r--r--
autorewrite.ml
10325
log
plain
-rw-r--r--
autorewrite.mli
2029
log
plain
-rw-r--r--
btermdn.ml
4671
log
plain
-rw-r--r--
btermdn.mli
1049
log
plain
-rw-r--r--
class_tactics.ml4
25919
log
plain
-rw-r--r--
contradiction.ml
2893
log
plain
-rw-r--r--
contradiction.mli
738
log
plain
-rw-r--r--
decl_interp.ml
16583
log
plain
-rw-r--r--
decl_interp.mli
770
log
plain
-rw-r--r--
decl_proof_instr.ml
45959
log
plain
-rw-r--r--
decl_proof_instr.mli
3828
log
plain
-rw-r--r--
dhyp.ml
10869
log
plain
-rw-r--r--
dhyp.mli
1082
log
plain
-rw-r--r--
dn.ml
2449
log
plain
-rw-r--r--
dn.mli
1319
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml4
16513
log
plain
-rw-r--r--
eauto.mli
1320
log
plain
-rw-r--r--
elim.ml
5628
log
plain
-rw-r--r--
elim.mli
1398
log
plain
-rw-r--r--
elimschemes.ml
4909
log
plain
-rw-r--r--
elimschemes.mli
1333
log
plain
-rw-r--r--
eqdecide.ml4
6289
log
plain
-rw-r--r--
eqschemes.ml
30806
log
plain
-rw-r--r--
eqschemes.mli
1882
log
plain
-rw-r--r--
equality.ml
53460
log
plain
-rw-r--r--
equality.mli
5222
log
plain
-rw-r--r--
evar_tactics.ml
2164
log
plain
-rw-r--r--
evar_tactics.mli
823
log
plain
-rw-r--r--
extraargs.ml4
11691
log
plain
-rw-r--r--
extraargs.mli
2407
log
plain
-rw-r--r--
extratactics.ml4
16770
log
plain
-rw-r--r--
extratactics.mli
765
log
plain
-rw-r--r--
hiddentac.ml
5335
log
plain
-rw-r--r--
hiddentac.mli
4700
log
plain
-rw-r--r--
hightactics.mllib
73
log
plain
-rw-r--r--
hipattern.ml4
16241
log
plain
-rw-r--r--
hipattern.mli
6499
log
plain
-rw-r--r--
inv.ml
18566
log
plain
-rw-r--r--
inv.mli
1536
log
plain
-rw-r--r--
leminv.ml
10621
log
plain
-rw-r--r--
leminv.mli
544
log
plain
-rw-r--r--
nbtermdn.ml
4599
log
plain
-rw-r--r--
nbtermdn.mli
1543
log
plain
-rw-r--r--
refine.ml
12735
log
plain
-rw-r--r--
refine.mli
593
log
plain
-rw-r--r--
rewrite.ml4
66150
log
plain
-rw-r--r--
tacinterp.ml
117189
log
plain
-rw-r--r--
tacinterp.mli
5718
log
plain
-rw-r--r--
tactic_option.ml
2157
log
plain
-rw-r--r--
tactic_option.mli
814
log
plain
-rw-r--r--
tacticals.ml
16092
log
plain
-rw-r--r--
tacticals.mli
8505
log
plain
-rw-r--r--
tactics.ml
131769
log
plain
-rw-r--r--
tactics.mli
14470
log
plain
-rw-r--r--
tactics.mllib
225
log
plain
-rw-r--r--
tauto.ml4
9462
log
plain
-rw-r--r--
termdn.ml
4241
log
plain
-rw-r--r--
termdn.mli
2363
log
plain