aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppvernac.ml')
-rw-r--r--printing/ppvernac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 418d4a0b8..e88284fb1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1223,7 +1223,7 @@ open Decl_kinds
let return = tag_vernac v in
match v with
| VernacExpr v' -> pr_vernac_expr v' ++ sep_end v'
- | VernacTime (_,v) ->
+ | VernacTime (_,(_,v)) ->
return (keyword "Time" ++ spc() ++ pr_vernac_control v)
| VernacRedirect (s, (_,v)) ->
return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)