From e3c247c1d96f39d2c07d120b69598a904b7d9f19 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Sun, 11 Jun 2017 15:14:15 +0200
Subject: deprecate Pp.std_ppcmds type alias

---
 lib/feedback.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/feedback.ml')

diff --git a/lib/feedback.ml b/lib/feedback.ml
index ed1d495d7..54d16a9be 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -32,7 +32,7 @@ type feedback_content =
   (* Extra metadata *)
   | Custom of Loc.t option * string * xml
   (* Generic messages *)
-  | Message of level * Loc.t option * Pp.std_ppcmds
+  | Message of level * Loc.t option * Pp.t
 
 type feedback = {
   id       : Stateid.t;
-- 
cgit v1.2.3