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.

---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 83296cf58f..203d913db8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1785,7 +1785,7 @@ let vernac_locate = let open Feedback in function
           (Constrextern.without_symbols pr_lglob_constr) ntn sc)
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> msg_notice (print_located_module qid)
-  | LocateTactic qid -> msg_notice (print_located_tactic qid)
+  | LocateOther (s, qid) -> msg_notice (print_located_other s qid)
   | LocateFile f -> msg_notice (locate_file f)
 
 let vernac_register id r =
-- 
cgit v1.2.3