diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 17:55:48 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-01 22:43:57 +0100 |
| commit | 967883e29a46a0fff9da8e56974468531948b174 (patch) | |
| tree | 9c9a814a92c2a7fb5006d478e6d20e16bcf74d7a /proofs/pfedit.mli | |
| parent | 3c8797a7e0d6536e28b8a8e7f4256241fc79dfc8 (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 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index d77ab667b..31e3d506b 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -126,7 +126,8 @@ val get_used_variables : unit -> Context.section_context option proof is focused or if there is no [n]th subgoal. [solve SelectAll tac] applies [tac] to all subgoals. *) -val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> unit Proofview.tactic -> +val solve : ?with_end_tac:unit Proofview.tactic -> + Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> Proof.proof -> Proof.proof*bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current |