diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index af65a1db0..999d25748 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -661,16 +661,8 @@ 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() ++ ps ++ + hov 2 (keyword "Notation" ++ spc() ++ qs s ++ str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++ (match opt with | None -> mt() |