diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-13 00:46:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:43:27 +0200 |
| commit | d28f2685615450c3c807764ce12bfdbe62450a01 (patch) | |
| tree | 7910f577a092b7a6c0fe983f6f64f01b79ffc20f /printing | |
| parent | 16b13e1aeac9559fc43939aa6d1d3f13a08daa14 (diff) | |
Printing notations as parsed.
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() |