aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/rtauto
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto')
-rw-r--r--plugins/rtauto/proof_search.mli4
1 files changed, 2 insertions, 2 deletions
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