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

---
 ide/interface.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'ide/interface.mli')

diff --git a/ide/interface.mli b/ide/interface.mli
index aab1d82728..1939a8427c 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -17,9 +17,9 @@ type verbose = bool
 type goal = {
   goal_id : string;
   (** Unique goal identifier *)
-  goal_hyp : Pp.std_ppcmds list;
+  goal_hyp : Pp.t list;
   (** List of hypotheses *)
-  goal_ccl : Pp.std_ppcmds;
+  goal_ccl : Pp.t;
   (** Goal conclusion *)
 }
 
@@ -121,7 +121,7 @@ type edit_id  = int
    should probably retract to that point *)
 type 'a value =
   | Good of 'a
-  | Fail of (state_id * location * Pp.std_ppcmds)
+  | Fail of (state_id * location * Pp.t)
 
 type ('a, 'b) union = ('a, 'b) Util.union
 
@@ -213,7 +213,7 @@ type about_sty = unit
 type about_rty = coq_info
 
 type handle_exn_sty = Exninfo.iexn
-type handle_exn_rty = state_id * location * Pp.std_ppcmds
+type handle_exn_rty = state_id * location * Pp.t
 
 (* Retrocompatibility stuff *)
 type interp_sty = (raw * verbose) * string
-- 
cgit v1.2.3