Fix double print in decl_mode.

After executing a command classified as VtProofStep the stm
prints the goals (if used via the tty API).

1 files changed, 3 insertions, 8 deletions

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 03929b3b8..acec8ba4e 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