From 8dbfee5c5f897af8186cb1bdfb04fd4f88eca677 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 11 Mar 2015 16:29:19 +0100
Subject: Fix double print in decl_mode.

After executing a command classified as VtProofStep the stm
prints the goals (if used via the tty API).
---
 plugins/decl_mode/g_decl_mode.ml4 | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 03929b3b86..acec8ba4e8 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -65,23 +65,18 @@ let vernac_decl_proof () =
   else
     begin
       Decl_proof_instr.go_to_proof_mode () ;
-      Proof_global.set_proof_mode "Declarative" ;
-      Vernacentries.print_subgoals ()
+      Proof_global.set_proof_mode "Declarative"
     end
 
 (* spiwack: some bureaucracy is not performed here *)
 let vernac_return () =
   begin
     Decl_proof_instr.return_from_tactic_mode () ;
-    Proof_global.set_proof_mode "Declarative" ;
-    Vernacentries.print_subgoals ()
+    Proof_global.set_proof_mode "Declarative"
   end
 
 let vernac_proof_instr instr =
-  begin
-    Decl_proof_instr.proof_instr instr;
-    Vernacentries.print_subgoals ()
-  end
+  Decl_proof_instr.proof_instr instr
 
 (* Before we can write an new toplevel command (see below) 
     which takes a [proof_instr] as argument, we need to declare
-- 
cgit v1.2.3