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
52287
log
plain
-rw-r--r--
auto.mli
9317
log
plain
-rw-r--r--
autorewrite.ml
10448
log
plain
-rw-r--r--
autorewrite.mli
2102
log
plain
-rw-r--r--
btermdn.ml
5029
log
plain
-rw-r--r--
btermdn.mli
1569
log
plain
-rw-r--r--
class_tactics.ml
25890
log
plain
-rw-r--r--
class_tactics.mli
1149
log
plain
-rw-r--r--
contradiction.ml
4000
log
plain
-rw-r--r--
contradiction.mli
705
log
plain
-rw-r--r--
dn.ml
2517
log
plain
-rw-r--r--
dn.mli
1221
log
plain
-rw-r--r--
doc.tex
246
log
plain
-rw-r--r--
eauto.ml4
19880
log
plain
-rw-r--r--
eauto.mli
1274
log
plain
-rw-r--r--
elim.ml
6019
log
plain
-rw-r--r--
elim.mli
1504
log
plain
-rw-r--r--
elimschemes.ml
4584
log
plain
-rw-r--r--
elimschemes.mli
1378
log
plain
-rw-r--r--
eqdecide.ml4
7774
log
plain
-rw-r--r--
eqschemes.ml
38364
log
plain
-rw-r--r--
eqschemes.mli
1878
log
plain
-rw-r--r--
equality.ml
64261
log
plain
-rw-r--r--
equality.mli
5781
log
plain
-rw-r--r--
evar_tactics.ml
2215
log
plain
-rw-r--r--
evar_tactics.mli
765
log
plain
-rw-r--r--
extraargs.ml4
12245
log
plain
-rw-r--r--
extraargs.mli
2589
log
plain
-rw-r--r--
extratactics.ml4
30188
log
plain
-rw-r--r--
extratactics.mli
799
log
plain
-rw-r--r--
g_class.ml4
2667
log
plain
-rw-r--r--
g_rewrite.ml4
12949
log
plain
-rw-r--r--
geninterp.ml
1195
log
plain
-rw-r--r--
geninterp.mli
1067
log
plain
-rw-r--r--
hightactics.mllib
84
log
plain
-rw-r--r--
hipattern.ml4
17454
log
plain
-rw-r--r--
hipattern.mli
6547
log
plain
-rw-r--r--
inv.ml
20995
log
plain
-rw-r--r--
inv.mli
1603
log
plain
-rw-r--r--
leminv.ml
10275
log
plain
-rw-r--r--
leminv.mli
1091
log
plain
-rw-r--r--
rewrite.ml
67221
log
plain
-rw-r--r--
rewrite.mli
2745
log
plain
-rw-r--r--
taccoerce.ml
8459
log
plain
-rw-r--r--
taccoerce.mli
2772
log
plain
-rw-r--r--
tacenv.ml
7887
log
plain
-rw-r--r--
tacenv.mli
2014
log
plain
-rw-r--r--
tacintern.ml
31678
log
plain
-rw-r--r--
tacintern.mli
2250
log
plain
-rw-r--r--
tacinterp.ml
82128
log
plain
-rw-r--r--
tacinterp.mli
4145
log
plain
-rw-r--r--
tacsubst.ml
14039
log
plain
-rw-r--r--
tacsubst.mli
1108
log
plain
-rw-r--r--
tacticMatching.ml
14071
log
plain
-rw-r--r--
tacticMatching.mli
2134
log
plain
-rw-r--r--
tactic_option.ml
1962
log
plain
-rw-r--r--
tactic_option.mli
790
log
plain
-rw-r--r--
tacticals.ml
23306
log
plain
-rw-r--r--
tacticals.mli
12070
log
plain
-rw-r--r--
tactics.ml
151317
log
plain
-rw-r--r--
tactics.mli
16793
log
plain
-rw-r--r--
tactics.mllib
226
log
plain
-rw-r--r--
tauto.ml4
12348
log
plain