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
7953
log
plain
-rw-r--r--
evar_tactics.ml
3144
log
plain
-rw-r--r--
evar_tactics.mli
883
log
plain
-rw-r--r--
extraargs.ml4
11045
log
plain
-rw-r--r--
extraargs.mli
2248
log
plain
-rw-r--r--
extratactics.ml4
35564
log
plain
-rw-r--r--
extratactics.mli
810
log
plain
-rw-r--r--
g_auto.ml4
6348
log
plain
-rw-r--r--
g_class.ml4
2746
log
plain
-rw-r--r--
g_eqdecide.ml4
1158
log
plain
-rw-r--r--
g_ltac.ml4
16090
log
plain
-rw-r--r--
g_obligations.ml4
5151
log
plain
-rw-r--r--
g_rewrite.ml4
12413
log
plain
-rw-r--r--
ltac.mllib
193
log
plain
-rw-r--r--
rewrite.ml
82295
log
plain
-rw-r--r--
rewrite.mli
3397
log
plain
-rw-r--r--
tacentries.ml
16675
log
plain
-rw-r--r--
tacentries.mli
2621
log
plain
-rw-r--r--
tacenv.ml
4379
log
plain
-rw-r--r--
tacenv.mli
2784
log
plain
-rw-r--r--
tacintern.ml
31300
log
plain
-rw-r--r--
tacintern.mli
2012
log
plain
-rw-r--r--
tacinterp.ml
83385
log
plain
-rw-r--r--
tacinterp.mli
4256
log
plain
-rw-r--r--
tacsubst.ml
12482
log
plain
-rw-r--r--
tacsubst.mli
1108
log
plain
-rw-r--r--
tactic_debug.ml
14035
log
plain
-rw-r--r--
tactic_debug.mli
3108
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
9520
log
plain
-rw-r--r--
tauto.mli
0
log
plain