From ed09ae7a473a99c914f2af64d3387d9190e85849 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 15 Dec 2017 04:15:55 +0100
Subject: [flags] Move global time flag into an attribute.

One less global flag.
---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

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)
-- 
cgit v1.2.3