From fefe98c314f89b8351af4fa3191242c702e6dc77 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 22 Jun 2012 09:21:59 +0000
Subject: A call to the command Proof (and its variants) now prints the
 subgoals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15472 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7b8d24c9d6..9c2e68fd4b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1576,9 +1576,9 @@ let interp c = match c with
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof (None, None) -> ()
-  | VernacProof (Some tac, None) -> vernac_set_end_tac tac
-  | VernacProof (None, Some l) -> vernac_set_used_variables l
+  | VernacProof (None, None) -> print_subgoals ()
+  | VernacProof (Some tac, None) -> vernac_set_end_tac tac ; print_subgoals ()
+  | VernacProof (None, Some l) -> vernac_set_used_variables l ; print_subgoals ()
   | VernacProof (Some tac, Some l) -> 
       vernac_set_end_tac tac; vernac_set_used_variables l
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
-- 
cgit v1.2.3