From 1682d4ed9df64937dfaa162e58233020036ff7b3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Feb 2017 13:23:15 +0100
Subject: Fixing #use"include" after vernac is added and ltac is moved to a
 plugin.

---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/top_printers.ml')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4fcad88202..dc354b130b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -234,7 +234,7 @@ let ppenvwithcst e = pp
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
    str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
 
-let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x))
+let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
 let ppobj obj = Format.print_string (Libobject.object_tag obj)
 
-- 
cgit v1.2.3