diff options
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 7b3491de22..b86f5ce660 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -489,6 +489,7 @@ let rec pr_vernac = function | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc() ++ qs s | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v + | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v (* Syntax *) | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e) |