Revert "Printing notations as parsed."

This reverts commit 92cbd4ed5f9679e46da16e83a2f920449c699a4e.

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()