aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/vernacexpr.mli1
1 files changed, 1 insertions, 0 deletions
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