From baef2bd34e1906ab56918c37a90c5468a4785656 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 31 Oct 2014 14:43:04 +0100
Subject: Show_script called only if in coqtop mode

---
 toplevel/vernacentries.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 90689aee6f..fb50a6bc22 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -485,7 +485,8 @@ let qed_display_script = ref true
 let vernac_end_proof ?proof = function
   | Admitted -> save_proof ?proof Admitted
   | Proved (_,_) as e ->
-    if is_verbose () && !qed_display_script then Stm.show_script ?proof ();
+    if is_verbose () && !qed_display_script && !Flags.coqtop_ui then
+      Stm.show_script ?proof ();
     save_proof ?proof e
 
   (* A stupid macro that should be replaced by ``Exact c. Save.'' all along
-- 
cgit v1.2.3