diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-10 14:32:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:43:27 +0200 |
| commit | 16b13e1aeac9559fc43939aa6d1d3f13a08daa14 (patch) | |
| tree | a8713e6018868ae599b001ac7dd462645fee5da3 /printing | |
| parent | c408cf73a6e170c7f4d3920427e4d4fdd4bef124 (diff) | |
So as to beautify to work, do not use notations in Inductive types
with a clause where, nor Notation, nor Fixpoints.
Should be certainly improved at least for Inductive types and
Fixpoints, depending on whether there is a "where" clause for
instance.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index cd7434843..af65a1db0 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -254,7 +254,8 @@ module Make | _ as c -> brk(0,2) ++ str" :" ++ pr_c c let pr_decl_notation prc ((loc,ntn),c,scopt) = - fnl () ++ keyword "where " ++ qs ntn ++ str " := " ++ prc c ++ + fnl () ++ keyword "where " ++ qs ntn ++ str " := " + ++ Flags.without_option Flags.beautify_file prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt let pr_binders_arg = @@ -670,7 +671,7 @@ module Make in return ( hov 2 (keyword "Notation" ++ spc() ++ ps ++ - str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++ + str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++ (match opt with | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) @@ -752,7 +753,7 @@ module Make let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ - pr_spc_lconstr c) + Flags.without_option Flags.beautify_file pr_spc_lconstr c) in let pr_constructor_list b l = match l with | Constructors [] -> mt() @@ -790,12 +791,14 @@ module Make | Some Local -> "Local " | None | Some Global -> "" in + let pr_pure_lconstr c = + Flags.without_option Flags.beautify_file pr_lconstr c in let pr_onerec = function | (((loc,id),pl),ro,bl,type_,def),ntn -> let annot = pr_guard_annot pr_lconstr_expr bl ro in pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ - ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++ + ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn in return ( |