diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 89ffae4b3e..832c08fe0e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -627,6 +627,8 @@ module Make ) | VernacTime v -> return (keyword "Time" ++ spc() ++ pr_vernac_list v) + | VernacRedirect (s, v) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v) | VernacFail v -> @@ -1253,7 +1255,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 +1273,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 |