diff options
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index e49f531f1..e177bb621 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -103,11 +103,8 @@ let pr_notation pr s env = let unpl, level = find_notation_printing_rule s in prlist (print_hunk pr env) unpl, level -let pr_delimiters sc strm = - match find_delimiters sc with - | None -> anomaly "Delimiters without concrete syntax" - | Some (left,right) -> - assert (left <> "" && right <> ""); +let pr_delimiters key strm = + let left = "`"^key^":" and right = "`" in let lspace = if is_letter (left.[String.length left -1]) then str " " else mt () in let rspace = |