diff options
| author | Hugo Herbelin | 2016-04-10 14:30:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-12 16:28:17 +0200 |
| commit | d78784bd86d3d571bb2891356e9e9718c69976ba (patch) | |
| tree | e3fe3966ffb0fa07721b6a33f4b653891098f970 | |
| parent | 907db7ee1c9824aeedad7ce2d0f4f85225c36aba (diff) | |
Fixing printing of "destruct in" after ce71ac17268f.
| -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 3cff541b06..19536d9f83 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) -> |