diff options
| author | Hugo Herbelin | 2016-10-11 22:11:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-12 11:00:13 +0200 |
| commit | 96ed527472c38e92727d8fb6bfc41770c43b762b (patch) | |
| tree | efb895c09b03b0359ad0b63ee44cff03ff4280b9 /printing | |
| parent | af3538f0c6decdccd47abcdeb7b7eeaff64b69b5 (diff) | |
Fixing a few confusions on the name of the beautify flag.
(It should apply also interactively.)
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f4a112a4cb..cfb4e79f03 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -263,7 +263,7 @@ module Make let pr_decl_notation prc ((loc,ntn),c,scopt) = fnl () ++ keyword "where " ++ qs ntn ++ str " := " - ++ Flags.without_option Flags.beautify_file prc c ++ + ++ Flags.without_option Flags.beautify prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt let pr_binders_arg = @@ -383,7 +383,7 @@ module Make | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}" let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) = - let pr_pure_lconstr c = Flags.without_option Flags.beautify_file pr_lconstr c in + let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in 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_ @@ -678,7 +678,7 @@ module Make | VernacNotation (_,c,((_,s),l),opt) -> return ( hov 2 (keyword "Notation" ++ spc() ++ qs s ++ - str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++ + str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++ (match opt with | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) @@ -760,7 +760,7 @@ module Make let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ - Flags.without_option Flags.beautify_file pr_spc_lconstr c) + Flags.without_option Flags.beautify pr_spc_lconstr c) in let pr_constructor_list b l = match l with | Constructors [] -> mt() |