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

---
 pretyping/detyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/detyping.ml')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f830d4be3..cac411183 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -81,7 +81,7 @@ let encode_tuple r =
 module PrintingInductiveMake =
   functor (Test : sig
      val encode : reference -> inductive
-     val member_message : std_ppcmds -> bool -> std_ppcmds
+     val member_message : Pp.t -> bool -> Pp.t
      val field : string
      val title : string
   end) ->
-- 
cgit v1.2.3