From f27df397b49d2bb469e513749cade21e5c259926 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Jul 2014 15:59:51 +0200
Subject: Adding a new "Locate Term" command, distinct from the raw "Locate"
 command. The new Term version has essentially the same behaviour as the old
 "Locate", while the new raw searches for all types of objects. Also code
 merging with the "Locate Ltac".

Fixes bug #3380.
---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5aa9d51fc3..f620652280 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -88,6 +88,7 @@ type searchable =
   | SearchAbout of (bool * search_about_item) list
 
 type locatable =
+  | LocateAny of reference or_by_notation
   | LocateTerm of reference or_by_notation
   | LocateLibrary of reference
   | LocateModule of reference
-- 
cgit v1.2.3