diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-01-23 17:16:23 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-01-23 17:16:23 +0100 |
commit | cfce4732363c7a93ffb7231335463d41c47074ea (patch) | |
tree | 0aa35e11b13dddcfd0fd7029f02e72d8e7df5c0c /printing/ppconstr.ml | |
parent | e91ae93106b6bd6d92ef53ac18b04654485a8106 (diff) | |
parent | a6f687852c0c7509a06fdf16c0af29129b3566d5 (diff) |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'printing/ppconstr.ml')
-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 aa94fb7be..80ddd669f 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 |