From 5822bdc9689620db3f9b7e5ea159d024cf213ba9 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Fri, 3 Jun 2016 08:04:38 +0200 Subject: Add goal range selectors. You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals numbered 1 and 3 to 5. --- engine/proofview.mli | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'engine/proofview.mli') diff --git a/engine/proofview.mli b/engine/proofview.mli index 7996b7969..2f8394e84 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -239,6 +239,16 @@ val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit val tclFOCUS : int -> int -> 'a tactic -> 'a tactic +(** [tclFOCUSLIST li t] applies [t] on the list of focused goals + described by [li]. Each element of [li] is a pair [(i, j)] denothing + the goals numbered from [i] to [j] (inclusive, starting from 1). + It will try to apply [t] to all the valid goals in any of these + intervals. If the set of such goals is not a single range, then it + will move goals such that it is a single range. (So, for + instance, [[1, 3-5]; idtac.] is not the identity.) + If the set of such goals is empty, it will fail. *) +val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic + (** [tclFOCUSID x t] applies [t] on a (single) focused goal like {!tclFOCUS}. The goal is found by its name rather than its number.*) -- cgit v1.2.3 From 1e19f163b8c7a21d63165784828f4d733aa95171 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Mon, 29 Jun 2015 14:11:06 +0200 Subject: Fix a typo in proofs/proofview.mli. --- engine/proofview.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/proofview.mli') diff --git a/engine/proofview.mli b/engine/proofview.mli index 2f8394e84..eecfcdefb 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -240,7 +240,7 @@ val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit val tclFOCUS : int -> int -> 'a tactic -> 'a tactic (** [tclFOCUSLIST li t] applies [t] on the list of focused goals - described by [li]. Each element of [li] is a pair [(i, j)] denothing + described by [li]. Each element of [li] is a pair [(i, j)] denoting the goals numbered from [i] to [j] (inclusive, starting from 1). It will try to apply [t] to all the valid goals in any of these intervals. If the set of such goals is not a single range, then it -- cgit v1.2.3