aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-01-23 17:16:23 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-01-23 17:16:23 +0100
commitcfce4732363c7a93ffb7231335463d41c47074ea (patch)
tree0aa35e11b13dddcfd0fd7029f02e72d8e7df5c0c /printing/ppconstr.ml
parente91ae93106b6bd6d92ef53ac18b04654485a8106 (diff)
parenta6f687852c0c7509a06fdf16c0af29129b3566d5 (diff)
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml2
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