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

---
 kernel/univ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 02b02db89..d915fb8c9 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -892,7 +892,7 @@ module Instance : sig
 
     val subst_fn : universe_level_subst_fn -> t -> t
     
-    val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+    val pr : (Level.t -> Pp.t) -> t -> Pp.t
     val levels : t -> LSet.t
 end = 
 struct
-- 
cgit v1.2.3