diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:43 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:43 +0000 |
| commit | 386d36deb6efb755cdd16ad216361e01e0b7662e (patch) | |
| tree | ad4a3063b901c508d759f9a9b9660a1e04dc1c3d /proofs/pfedit.mli | |
| parent | e6404437c1f6ae451f4253cd3450f75513b395c3 (diff) | |
Adds a new goal selector "all:".
all:tac applies tac to all the focused subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16982 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 73f12db98..f7c7b3653 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -120,7 +120,7 @@ val get_all_proof_names : unit -> Id.t list (** {6 ... } *) (** [set_end_tac tac] applies tactic [tac] to all subgoal generate - by [solve_nth] *) + by [solve] *) val set_end_tac : Tacexpr.raw_tactic_expr -> unit @@ -131,17 +131,18 @@ val set_used_variables : Id.t list -> unit val get_used_variables : unit -> Context.section_context option (** {6 ... } *) -(** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the - current focused proof or raises a UserError if no proof is focused or - if there is no [n]th subgoal *) +(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th + subgoal of the current focused proof or raises a [UserError] if no + proof is focused or if there is no [n]th subgoal. [solve SelectAll + tac] applies [tac] to all subgoals. *) -val solve_nth : ?with_end_tac:unit Proofview.tactic -> int -> unit Proofview.tactic -> +val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> unit Proofview.tactic -> Proof.proof -> Proof.proof*bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current - focused proof or raises a UserError if there is no focused proof or - if there is no more subgoals. - Returns [false] if an unsafe tactic has been used. *) + focused proof or raises a UserError if there is no focused proof or + if there is no more subgoals. + Returns [false] if an unsafe tactic has been used. *) val by : unit Proofview.tactic -> bool |