From c864695069da8f83a488261d9e842bfba970d114 Mon Sep 17 00:00:00 2001
From: courtieu
Date: Fri, 28 Apr 2006 14:51:42 +0000
Subject: If function creates proof obligation, there are now printed once.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8769 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/recdef/recdef.ml4 | 1 +
 1 file changed, 1 insertion(+)

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index cf09e63a75..febc14d386 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -850,6 +850,7 @@ let open_new_goal ref goal_name (gls_type,decompose_and_tac,nb_goal)   =
     gls_type 
     hook ;
   by (decompose_and_tac);
+  pp (Printer.pr_open_subgoals());
   ()
     
 let com_terminate ref is_mes fonctional_ref input_type relation rec_arg_num
-- 
cgit v1.2.3