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

---
 dev/doc/changes.txt | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 57c7a97d58..a48c491d33 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -18,6 +18,10 @@ We changed the type of the following functions:
   The returned term contains De Bruijn universe variables.
 - Global.body_of_constant: same as above.
 
+We renamed the following datatypes:
+
+  Pp.std_ppcmds -> Pp.t
+
 =========================================
 = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
 =========================================
-- 
cgit v1.2.3