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.
---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ae9328fcc0..029ee8a480 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -29,6 +29,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
    similar, they do not seem to mean the same thing. *)
 type goal_selector =
   | SelectNth of int
+  | SelectList of (int * int) list
   | SelectId of Id.t
   | SelectAll
 
-- 
cgit v1.2.3