diff options
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 3cff541b0..19536d9f8 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -878,7 +878,7 @@ module Make ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) -> pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++ pr_with_induction_names pr.pr_dconstr ids ++ - pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++ + pr_opt (pr_clauses None pr.pr_name) cl) l ++ pr_opt pr_eliminator el ) | TacDoubleInduction (h1,h2) -> |