From 1cf1fb46904d149a4f8e597735ed4fb1b4ff24d3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:03 +0200
Subject: Revert "Printing notations as parsed."

This reverts commit 92cbd4ed5f9679e46da16e83a2f920449c699a4e.
---
 printing/ppvernac.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

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()
-- 
cgit v1.2.3