diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 6d7e3c38d9..16759a3d83 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -531,13 +531,9 @@ let rec pr_vernac = function | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s (* Control *) - | VernacList l -> - hov 2 (str"[" ++ spc() ++ - prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l - ++ spc() ++ str"]") | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc() ++ qs s - | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v + | VernacTime v -> str"Time" ++ spc() ++ pr_vernac_list v | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v | VernacError _ -> str"No-parsing-rule for VernacError" @@ -959,6 +955,11 @@ let rec pr_vernac = function | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i | VernacEndSubproof -> str "}" +and pr_vernac_list l = + hov 2 (str"[" ++ spc() ++ + prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l + ++ spc() ++ str"]") + and pr_extend s cl = let pr_arg a = try pr_gen a |