From 8326639ef45b22cb066f65d17f27a77a678eb694 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Aug 2014 13:08:08 +0200
Subject: Add syntax [id]: to apply tactic to goal named id.

---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index b784bc4334..009ec543c8 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
 
-- 
cgit v1.2.3