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

---
 vernac/explainErr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/explainErr.ml')

diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 793a4c580..2178a7caa 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -18,7 +18,7 @@ let guill s = str "\"" ++ str s ++ str "\""
 (** Invariant : exceptions embedded in EvaluatedError satisfy
     Errors.noncritical *)
 
-exception EvaluatedError of std_ppcmds * exn option
+exception EvaluatedError of Pp.t * exn option
 
 (** Registration of generic errors
     Nota: explain_exn does NOT end with a newline anymore!
-- 
cgit v1.2.3