diff options
| author | Pierre-Marie Pédrot | 2017-02-01 10:52:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-01 10:54:53 +0100 |
| commit | c17c3faee20251cd5c7168246e9ffcd12d557f85 (patch) | |
| tree | 02635866b73d7595fad009cc17535a6bbf06c2fc /printing | |
| parent | f86bfa39cddfb9c6411ed8624cee9a2b5c8d53bd (diff) | |
| parent | 568b38e1d599f8bac5adf140f5a114f2871bc436 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index aa94fb7be3..80ddd669f4 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -442,7 +442,7 @@ end) = struct let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = if dangling_with_for then pr_dangling else pr in - pr_id id ++ str" " ++ + pr_id id ++ (if bl = [] then mt () else str" ") ++ hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++ pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c |
