diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-03 08:04:38 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-14 06:21:30 +0200 |
| commit | 5822bdc9689620db3f9b7e5ea159d024cf213ba9 (patch) | |
| tree | 0fae337d395c9bfe589e8a7aae99f32f6baf822f /intf | |
| parent | 19330a458b907b5e66a967adbfe572d92194913c (diff) | |
Add goal range selectors.
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ae9328fcc..029ee8a48 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 |