diff options
| author | Hugo Herbelin | 2020-02-14 13:01:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-04 11:56:40 +0100 |
| commit | fb9442de3a7f5cab102f33a342a5fc7f63cd8f1c (patch) | |
| tree | 5d4aa2080df69642bd2121e8c4a2576a2b9cfbb5 /vernac/ppvernac.ml | |
| parent | 89f111f2e15d8cab61495a419f0c9f7ae95e086a (diff) | |
Adding support for an "only parsing" modifier in "where"-based notations.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 33d9e3d98a..48961fd271 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -297,11 +297,6 @@ open Pputils | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c - let pr_decl_notation prc ({loc; v=ntn},c,scopt) = - fnl () ++ keyword "where " ++ qs ntn ++ str " := " - ++ Flags.without_option Flags.beautify prc c ++ - pr_opt (fun sc -> str ": " ++ str sc) scopt - let pr_binders_arg = let env = Global.env () in let sigma = Evd.from_env env in @@ -418,6 +413,15 @@ let string_of_theorem_kind = let open Decls in function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") + let pr_only_parsing_clause onlyparsing = + pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []) + + let pr_decl_notation prc ({loc; v=ntn},c,onlyparsing, scopt) = + fnl () ++ keyword "where " ++ qs ntn ++ str " := " + ++ Flags.without_option Flags.beautify prc c + ++ pr_only_parsing_clause onlyparsing + ++ pr_opt (fun sc -> str ": " ++ str sc) scopt + let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } = let env = Global.env () in let sigma = Evd.from_env env in @@ -1057,7 +1061,7 @@ let string_of_definition_object_kind = let open Decls in function hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ - pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) + pr_only_parsing_clause onlyparsing) ) | VernacArguments (q, args, more_implicits, mods) -> return ( |