From 967883e29a46a0fff9da8e56974468531948b174 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 5 Aug 2014 17:55:48 +0200 Subject: 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). --- proofs/pfedit.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'proofs/pfedit.mli') 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 -- cgit v1.2.3