From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- plugins/rtauto/proof_search.ml | 4 ++-- plugins/rtauto/proof_search.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/rtauto') diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index d773b153..576f7d4e 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -509,8 +509,8 @@ let pp_gl gl= cut () ++ let pp = function - Incomplete(gl,ctx) -> msgnl (pp_gl gl) - | _ -> msg (str "") + Incomplete(gl,ctx) -> pp_gl gl ++ fnl () + | _ -> str "" let pp_info () = let count_info = diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index b236aa72..275e94cd 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -38,7 +38,7 @@ val branching: state -> state list val success: state -> bool -val pp: state -> unit +val pp: state -> Pp.std_ppcmds val pr_form : form -> unit -- cgit v1.2.3