index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
ltac
Mode
Name
Size
-rw-r--r--
Ltac.v
0
log
plain
-rw-r--r--
coretactics.ml4
10220
log
plain
-rw-r--r--
evar_tactics.ml
3984
log
plain
-rw-r--r--
evar_tactics.mli
932
log
plain
-rw-r--r--
extraargs.ml4
13395
log
plain
-rw-r--r--
extraargs.mli
2631
log
plain
-rw-r--r--
extratactics.ml4
38396
log
plain
-rw-r--r--
extratactics.mli
811
log
plain
-rw-r--r--
g_auto.ml4
7085
log
plain
-rw-r--r--
g_class.ml4
3897
log
plain
-rw-r--r--
g_eqdecide.ml4
1159
log
plain
-rw-r--r--
g_ltac.ml4
18947
log
plain
-rw-r--r--
g_obligations.ml4
5621
log
plain
-rw-r--r--
g_rewrite.ml4
13057
log
plain
-rw-r--r--
g_tactic.ml4
27825
log
plain
-rw-r--r--
ltac_plugin.mlpack
278
log
plain
-rw-r--r--
pltac.ml
2514
log
plain
-rw-r--r--
pltac.mli
1758
log
plain
-rw-r--r--
pptactic.ml
52637
log
plain
-rw-r--r--
pptactic.mli
4866
log
plain
-rw-r--r--
profile_ltac.ml
15084
log
plain
-rw-r--r--
profile_ltac.mli
1861
log
plain
-rw-r--r--
profile_ltac_tactics.ml4
1471
log
plain
-rw-r--r--
rewrite.ml
84641
log
plain
-rw-r--r--
rewrite.mli
3522
log
plain
-rw-r--r--
tacarg.ml
929
log
plain
-rw-r--r--
tacarg.mli
1177
log
plain
-rw-r--r--
taccoerce.ml
12054
log
plain
-rw-r--r--
taccoerce.mli
3323
log
plain
-rw-r--r--
tacentries.ml
19128
log
plain
-rw-r--r--
tacentries.mli
2862
log
plain
-rw-r--r--
tacenv.ml
5228
log
plain
-rw-r--r--
tacenv.mli
3136
log
plain
-rw-r--r--
tacexpr.mli
11841
log
plain
-rw-r--r--
tacintern.ml
32040
log
plain
-rw-r--r--
tacintern.mli
2028
log
plain
-rw-r--r--
tacinterp.ml
83054
log
plain
-rw-r--r--
tacinterp.mli
5339
log
plain
-rw-r--r--
tacsubst.ml
12609
log
plain
-rw-r--r--
tacsubst.mli
1108
log
plain
-rw-r--r--
tactic_debug.ml
15043
log
plain
-rw-r--r--
tactic_debug.mli
3120
log
plain
-rw-r--r--
tactic_matching.ml
15038
log
plain
-rw-r--r--
tactic_matching.mli
2223
log
plain
-rw-r--r--
tactic_option.ml
1962
log
plain
-rw-r--r--
tactic_option.mli
781
log
plain
-rw-r--r--
tauto.ml
9829
log
plain
-rw-r--r--
tauto.mli
0
log
plain
-rw-r--r--
tauto_plugin.mlpack
6
log
plain