diff options
| author | Hugo Herbelin | 2016-04-13 00:46:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:47 +0200 |
| commit | 92cbd4ed5f9679e46da16e83a2f920449c699a4e (patch) | |
| tree | 34cde0bf35733276e41ba4bf000412bb1ee17ee5 | |
| parent | fd8669f9f2e37607f5eba56ba25e267711876e62 (diff) | |
Printing notations as parsed.
| -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 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() |