diff options
| author | Hugo Herbelin | 2020-10-06 00:18:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:00:24 +0200 |
| commit | d98cca66ea0e64193e7f79ffcf99b632d0ad6f14 (patch) | |
| tree | 37d88269b02de930a3eb2dc62f6f1cbbcdb94942 /vernac/ppvernac.ml | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Closes #13142 (more standardized pretty-printing of records).
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f972e05d3b..e9cd4272e6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -524,8 +524,7 @@ let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = n prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr) ntn let pr_record_decl c fs = - pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") + pr_opt pr_lident c ++ pr_record "{" "}" pr_record_field fs let pr_printable = function | PrintFullContext -> @@ -966,7 +965,7 @@ let pr_vernac_expr v = str":" ++ spc () ++ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with - | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ pr_record_body "{" "}" pr_lconstr l | Some (true,_) -> assert false | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) |