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.

---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/ppvernac.ml')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 10dd42ea91..a1cdfdbaa2 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1156,7 +1156,7 @@ open Decl_kinds
           | LocateFile f -> keyword "File" ++ spc() ++ qs f
           | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
           | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
-          | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid
+          | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid
         in
         return (keyword "Locate" ++ spc() ++ pr_locate loc)
       | VernacRegister (id, RegisterInline) ->
-- 
cgit v1.2.3