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
51462
log
plain
-rw-r--r--
auto.mli
9312
log
plain
-rw-r--r--
autorewrite.ml
10397
log
plain
-rw-r--r--
autorewrite.mli
2003
log
plain
-rw-r--r--
btermdn.ml
4579
log
plain
-rw-r--r--
btermdn.mli
1024
log
plain
-rw-r--r--
class_tactics.ml4
28060
log
plain
-rw-r--r--
contradiction.ml
2885
log
plain
-rw-r--r--
contradiction.mli
714
log
plain
-rw-r--r--
dhyp.ml
10912
log
plain
-rw-r--r--
dhyp.mli
1059
log
plain
-rw-r--r--
dn.ml
2449
log
plain
-rw-r--r--
dn.mli
1322
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml4
17537
log
plain
-rw-r--r--
eauto.mli
1322
log
plain
-rw-r--r--
elim.ml
5439
log
plain
-rw-r--r--
elim.mli
1379
log
plain
-rw-r--r--
elimschemes.ml
4897
log
plain
-rw-r--r--
elimschemes.mli
1378
log
plain
-rw-r--r--
eqdecide.ml4
6173
log
plain
-rw-r--r--
eqschemes.ml
37881
log
plain
-rw-r--r--
eqschemes.mli
1822
log
plain
-rw-r--r--
equality.ml
57892
log
plain
-rw-r--r--
equality.mli
5401
log
plain
-rw-r--r--
evar_tactics.ml
2028
log
plain
-rw-r--r--
evar_tactics.mli
756
log
plain
-rw-r--r--
extraargs.ml4
11472
log
plain
-rw-r--r--
extraargs.mli
2885
log
plain
-rw-r--r--
extratactics.ml4
26693
log
plain
-rw-r--r--
extratactics.mli
751
log
plain
-rw-r--r--
hiddentac.ml
5769
log
plain
-rw-r--r--
hiddentac.mli
4845
log
plain
-rw-r--r--
hightactics.mllib
73
log
plain
-rw-r--r--
hipattern.ml4
16344
log
plain
-rw-r--r--
hipattern.mli
6510
log
plain
-rw-r--r--
inv.ml
18627
log
plain
-rw-r--r--
inv.mli
1510
log
plain
-rw-r--r--
leminv.ml
10022
log
plain
-rw-r--r--
leminv.mli
546
log
plain
-rw-r--r--
nbtermdn.ml
4590
log
plain
-rw-r--r--
nbtermdn.mli
1502
log
plain
-rw-r--r--
refine.ml
13029
log
plain
-rw-r--r--
refine.mli
579
log
plain
-rw-r--r--
rewrite.ml4
77115
log
plain
-rw-r--r--
tacinterp.ml
117921
log
plain
-rw-r--r--
tacinterp.mli
5795
log
plain
-rw-r--r--
tactic_option.ml
2173
log
plain
-rw-r--r--
tactic_option.mli
791
log
plain
-rw-r--r--
tacticals.ml
16017
log
plain
-rw-r--r--
tacticals.mli
8467
log
plain
-rw-r--r--
tactics.ml
134194
log
plain
-rw-r--r--
tactics.mli
14920
log
plain
-rw-r--r--
tactics.mllib
196
log
plain
-rw-r--r--
tauto.ml4
9505
log
plain
-rw-r--r--
termdn.ml
4014
log
plain
-rw-r--r--
termdn.mli
2333
log
plain