From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 plugins/ltac/g_rewrite.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac/g_rewrite.ml4')

diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index fbaa2e58..f1634f15 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -11,7 +11,6 @@
 (* Syntax for rewriting with strategies *)
 
 open Names
-open Misctypes
 open Locus
 open Constrexpr
 open Glob_term
@@ -20,9 +19,10 @@ open Extraargs
 open Tacmach
 open Rewrite
 open Stdarg
-open Pcoq.Vernac_
+open Tactypes
 open Pcoq.Prim
 open Pcoq.Constr
+open Pvernac.Vernac_
 open Pltac
 
 DECLARE PLUGIN "ltac_plugin"
@@ -67,13 +67,13 @@ let subst_strategy s str = str
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
 let pr_raw_strategy prc prlc _ (s : raw_strategy) =
-  let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in
+  let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
   Rewrite.pr_strategy prc prr s
 let pr_glob_strategy prc prlc _ (s : glob_strategy) =
   let prr = Pptactic.pr_red_expr
     (Ppconstr.pr_constr_expr,
     Ppconstr.pr_lconstr_expr,
-    Pputils.pr_or_by_notation Libnames.pr_reference,
+    Pputils.pr_or_by_notation Libnames.pr_qualid,
     Ppconstr.pr_constr_expr)
   in
   Rewrite.pr_strategy prc prr s
-- 
cgit v1.2.3