From 1522090b4cd7a8b7c7e83e316c79bc8c06ab62e9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 27 Nov 2019 17:14:51 -0500
Subject: Make the string argument of `time` print correctly

Fixes #10971
---
 plugins/ltac/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6df068883c..e0b702ba89 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -971,7 +971,7 @@ let pr_goal_selector ~toplevel s =
             | TacTime (s,t) ->
               hov 1 (
                 keyword "time"
-                ++ pr_opt str s ++ spc ()
+                ++ pr_opt qstring s ++ spc ()
                 ++ pr_tac (ltactical,E) t),
               ltactical
             | TacRepeat t ->
-- 
cgit v1.2.3