diff options
Diffstat (limited to 'plugins/rtauto')
-rw-r--r-- | plugins/rtauto/proof_search.ml | 4 | ||||
-rw-r--r-- | plugins/rtauto/proof_search.mli | 2 |
2 files changed, 3 insertions, 3 deletions
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 "<complete>") + Incomplete(gl,ctx) -> pp_gl gl ++ fnl () + | _ -> str "<complete>" 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 |