From 92cbd4ed5f9679e46da16e83a2f920449c699a4e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Apr 2016 00:46:04 +0200
Subject: Printing notations as parsed.

---
 printing/ppvernac.ml | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 0e68c961f5..d5934e1217 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -665,16 +665,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()
-- 
cgit v1.2.3