aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/tQueue.mli
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-08-05 17:55:48 +0200
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-11-01 22:43:57 +0100
commit967883e29a46a0fff9da8e56974468531948b174 (patch)
tree9c9a814a92c2a7fb5006d478e6d20e16bcf74d7a /stm/tQueue.mli
parent3c8797a7e0d6536e28b8a8e7f4256241fc79dfc8 (diff)
Add [Info] command.
Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
Diffstat (limited to 'stm/tQueue.mli')
0 files changed, 0 insertions, 0 deletions