Add goal range selectors.

You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.

1 files changed, 10 insertions, 0 deletions

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.*)