From 1a6a26d29252da54b86bf663a66ddd909905d1cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 Oct 2017 14:06:29 +0200
Subject: Moving the Ltac-specific part of the nametab to the Ltac plugin.

For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.
---
 plugins/ltac/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/pptactic.ml')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d8bd166208..d588c888c4 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -336,7 +336,7 @@ type 'a extra_genarg_printer =
   let pr_ltac_constant kn =
     if !Flags.in_debugger then KerName.print kn
     else try
-           pr_qualid (Nametab.shortest_qualid_of_tactic kn)
+           pr_qualid (Tacenv.shortest_qualid_of_tactic kn)
       with Not_found -> (* local tactic not accessible anymore *)
         str "<" ++ KerName.print kn ++ str ">"
 
-- 
cgit v1.2.3