index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
Mode
Name
Size
-rw-r--r--
coretactics.ml4
9142
log
plain
-rw-r--r--
evar_tactics.ml
3201
log
plain
-rw-r--r--
evar_tactics.mli
883
log
plain
-rw-r--r--
extraargs.ml4
12339
log
plain
-rw-r--r--
extraargs.mli
2411
log
plain
-rw-r--r--
extratactics.ml4
36612
log
plain
-rw-r--r--
extratactics.mli
810
log
plain
-rw-r--r--
g_auto.ml4
6352
log
plain
-rw-r--r--
g_class.ml4
3596
log
plain
-rw-r--r--
g_eqdecide.ml4
1158
log
plain
-rw-r--r--
g_ltac.ml4
19073
log
plain
-rw-r--r--
g_obligations.ml4
5653
log
plain
-rw-r--r--
g_rewrite.ml4
12293
log
plain
-rw-r--r--
g_tactic.ml4
25115
log
plain
-rw-r--r--
ltac.mllib
284
log
plain
-rw-r--r--
pltac.ml
2498
log
plain
-rw-r--r--
pltac.mli
1690
log
plain
-rw-r--r--
pptactic.ml
50169
log
plain
-rw-r--r--
pptactic.mli
2191
log
plain
-rw-r--r--
pptacticsig.mli
2682
log
plain
-rw-r--r--
profile_ltac.ml
14331
log
plain
-rw-r--r--
profile_ltac.mli
1806
log
plain
-rw-r--r--
profile_ltac_tactics.ml4
1349
log
plain
-rw-r--r--
rewrite.ml
82549
log
plain
-rw-r--r--
rewrite.mli
3427
log
plain
-rw-r--r--
tacarg.ml
929
log
plain
-rw-r--r--
tacarg.mli
1177
log
plain
-rw-r--r--
taccoerce.ml
11356
log
plain
-rw-r--r--
taccoerce.mli
3125
log
plain
-rw-r--r--
tacentries.ml
17874
log
plain
-rw-r--r--
tacentries.mli
2735
log
plain
-rw-r--r--
tacenv.ml
4286
log
plain
-rw-r--r--
tacenv.mli
2784
log
plain
-rw-r--r--
tacexpr.mli
11819
log
plain
-rw-r--r--
tacintern.ml
31244
log
plain
-rw-r--r--
tacintern.mli
2012
log
plain
-rw-r--r--
tacinterp.ml
83096
log
plain
-rw-r--r--
tacinterp.mli
4406
log
plain
-rw-r--r--
tacsubst.ml
12502
log
plain
-rw-r--r--
tacsubst.mli
1108
log
plain
-rw-r--r--
tactic_debug.ml
14470
log
plain
-rw-r--r--
tactic_debug.mli
3108
log
plain
-rw-r--r--
tactic_matching.ml
15048
log
plain
-rw-r--r--
tactic_matching.mli
2199
log
plain
-rw-r--r--
tactic_option.ml
1962
log
plain
-rw-r--r--
tactic_option.mli
790
log
plain
-rw-r--r--
tauto.ml
9513
log
plain
-rw-r--r--
tauto.mli
0
log
plain