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
10229
log
plain
-rw-r--r--
evar_tactics.ml
4018
log
plain
-rw-r--r--
evar_tactics.mli
941
log
plain
-rw-r--r--
extraargs.ml4
13358
log
plain
-rw-r--r--
extraargs.mli
2697
log
plain
-rw-r--r--
extratactics.ml4
38460
log
plain
-rw-r--r--
extratactics.mli
820
log
plain
-rw-r--r--
g_auto.ml4
6896
log
plain
-rw-r--r--
g_class.ml4
3868
log
plain
-rw-r--r--
g_eqdecide.ml4
1167
log
plain
-rw-r--r--
g_ltac.ml4
19478
log
plain
-rw-r--r--
g_obligations.ml4
5637
log
plain
-rw-r--r--
g_rewrite.ml4
12717
log
plain
-rw-r--r--
g_tactic.ml4
27851
log
plain
-rw-r--r--
ltac_plugin.mlpack
284
log
plain
-rw-r--r--
pltac.ml
2540
log
plain
-rw-r--r--
pltac.mli
1784
log
plain
-rw-r--r--
pptactic.ml
47634
log
plain
-rw-r--r--
pptactic.mli
3845
log
plain
-rw-r--r--
profile_ltac.ml
14443
log
plain
-rw-r--r--
profile_ltac.mli
1870
log
plain
-rw-r--r--
profile_ltac_tactics.ml4
1483
log
plain
-rw-r--r--
rewrite.ml
84040
log
plain
-rw-r--r--
rewrite.mli
3539
log
plain
-rw-r--r--
tacarg.ml
938
log
plain
-rw-r--r--
tacarg.mli
1186
log
plain
-rw-r--r--
taccoerce.ml
11603
log
plain
-rw-r--r--
taccoerce.mli
3310
log
plain
-rw-r--r--
tacentries.ml
18010
log
plain
-rw-r--r--
tacentries.mli
2787
log
plain
-rw-r--r--
tacenv.ml
4306
log
plain
-rw-r--r--
tacenv.mli
2781
log
plain
-rw-r--r--
tacexpr.mli
11833
log
plain
-rw-r--r--
tacintern.ml
31386
log
plain
-rw-r--r--
tacintern.mli
2068
log
plain
-rw-r--r--
tacinterp.ml
82313
log
plain
-rw-r--r--
tacinterp.mli
5142
log
plain
-rw-r--r--
tacsubst.ml
12569
log
plain
-rw-r--r--
tacsubst.mli
1117
log
plain
-rw-r--r--
tactic_debug.ml
14895
log
plain
-rw-r--r--
tactic_debug.mli
3165
log
plain
-rw-r--r--
tactic_matching.ml
15069
log
plain
-rw-r--r--
tactic_matching.mli
2227
log
plain
-rw-r--r--
tactic_option.ml
1971
log
plain
-rw-r--r--
tactic_option.mli
799
log
plain
-rw-r--r--
tauto.ml
9814
log
plain
-rw-r--r--
tauto.mli
0
log
plain