diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-01-05 19:54:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-01-05 20:13:00 +0100 |
| commit | 65816f94ba427edf8999bf42633d0aad064e8ce4 (patch) | |
| tree | 80c9b34a1c2ba5af338a1409473475c5af277890 /printing/ppconstr.ml | |
| parent | 63ca4aac83ced14b9b8065ef43e29f7c2dfd331c (diff) | |
Fixing a little bug in printing cofix with no arguments.
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 e21bfa007..31d87f0ff 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -418,7 +418,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 |