diff options
| -rw-r--r-- | printing/ppvernac.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index d5934e1217..0e68c961f5 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -665,8 +665,16 @@ module Make | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) ) | VernacNotation (_,c,((_,s),l),opt) -> + let ps = + let n = String.length s in + if n > 2 && s.[0] == '\'' && s.[n-1] == '\'' + then + let s' = String.sub s 1 (n-2) in + if String.contains s' '\'' then qs s else str s' + else qs s + in return ( - hov 2 (keyword "Notation" ++ spc() ++ qs s ++ + hov 2 (keyword "Notation" ++ spc() ++ ps ++ str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++ (match opt with | None -> mt() |