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 --- plugins/rtauto/proof_search.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/rtauto') diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index e0c09f394..86231cf19 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -38,9 +38,9 @@ val branching: state -> state list val success: state -> bool -val pp: state -> Pp.std_ppcmds +val pp: state -> Pp.t -val pr_form : form -> Pp.std_ppcmds +val pr_form : form -> Pp.t val reset_info : unit -> unit -- cgit v1.2.3