diff options
| author | coqbot-app[bot] | 2020-10-15 11:13:43 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-15 11:13:43 +0000 |
| commit | 56384cc09d6d9e9446e7c11aee5def865e28a4d5 (patch) | |
| tree | 46a673c5b4601f8d1fb93421945b504642b9a6bb /vernac | |
| parent | 411025844a4c005ce03d77c6c640807c28269d4a (diff) | |
| parent | d98cca66ea0e64193e7f79ffcf99b632d0ad6f14 (diff) | |
Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq records
Reviewed-by: ejgallego
Ack-by: SkySkimmer
Diffstat (limited to 'vernac')
| -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())) |