aboutsummaryrefslogtreecommitdiffhomepage
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 b784bc433..009ec543c 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -30,6 +30,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
+ | SelectId of Id.t
| SelectAll
| SelectAllParallel