diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 89ffae4b3..c6b1b672f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1253,7 +1253,7 @@ module Make and pr_extend s cl = let pr_arg a = try pr_gen a - with Failure _ -> str ("<error in "^fst s^">") in + with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in try let rl = Egramml.get_extend_vernac_rule s in let start,rl,cl = @@ -1271,7 +1271,7 @@ module Make (start,cl) rl in hov 1 pp with Not_found -> - hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") + hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") in pr_vernac |