From 24a125b779c0cf6e9b0662e122c74aa80eb1837b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 08:21:36 +0200
Subject: Remove extraneous space in coqtop/pg output (bug #4675).

---
 printing/printer.ml | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 4e740bffe2..8469490f05 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -381,16 +381,12 @@ let pr_transparent_state (ids, csts) =
 let default_pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
   let env = Goal.V82.env sigma g in
-  let preamb,thesis,penv,pc =
-    mt (), mt (),
-    pr_context_of env sigma,
-    pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
-  in
-    preamb ++
-    str"  " ++ hv 0 (penv ++ fnl () ++
-		       str (emacs_str "")  ++
-		       str "============================" ++ fnl ()  ++
-		       thesis ++ str " " ++  pc)
+  let concl = Goal.V82.concl sigma g in
+  let goal =
+    pr_context_of env sigma ++ cut () ++
+      str "============================" ++ cut ()  ++
+      pr_goal_concl_style_env env sigma concl in
+  str "  " ++ v 0 goal
 
 (* display a goal tag *)
 let pr_goal_tag g =
-- 
cgit v1.2.3