diff options
| author | courtieu | 2006-04-28 14:51:42 +0000 |
|---|---|---|
| committer | courtieu | 2006-04-28 14:51:42 +0000 |
| commit | c864695069da8f83a488261d9e842bfba970d114 (patch) | |
| tree | 8cb0f99e4594cc22d6c17ee9eaa005736f9077aa | |
| parent | 78fff376f71ce6538dad42be95b074a916a4ce49 (diff) | |
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
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
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 |