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