diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index c6b1b672f..832c08fe0 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 -> |