diff options
| author | Hugo Herbelin | 2016-04-09 16:14:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-09 18:26:00 +0200 |
| commit | b5cc4ac65764b0866bf57caa6f9aa7fa631eabf1 (patch) | |
| tree | 8e562ed97d1f20419e1569b52a357611314f60af | |
| parent | ce71ac17268f11ddd92f4bea85cbdd9c62acbc21 (diff) | |
Fixing extra space in printing inductive types with no explicit type given.
| -rw-r--r-- | printing/ppvernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 55f8f909f0..0b761881dc 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -778,8 +778,8 @@ module Make hov 0 ( str key ++ spc() ++ (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++ - pr_and_type_binders_arg indpar ++ spc() ++ - Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ + pr_and_type_binders_arg indpar ++ + pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++ str" :=") ++ pr_constructor_list k lc ++ prlist (pr_decl_notation pr_constr) ntn in |