From 811ed22e8dcb12d8c88e2c320bbc2221bdff30ab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 Oct 2017 15:09:21 +0200
Subject: Implementing a generic mechanism for locating named objects from Coq
 side.

---
 intf/vernacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 03e8ea43d1..4a471d4a2b 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -91,7 +91,7 @@ type locatable =
   | LocateTerm of reference or_by_notation
   | LocateLibrary of reference
   | LocateModule of reference
-  | LocateTactic of reference
+  | LocateOther of string * reference
   | LocateFile of string
 
 type showable =
-- 
cgit v1.2.3