diff options
| -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 |