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
---
 .gitignore                                           |  1 +
 doc/changelog/04-tactics/11203-fix-time-printing.rst |  4 ++++
 plugins/ltac/pptactic.ml                             |  2 +-
 test-suite/output/print_ltac.out                     |  8 ++++++++
 test-suite/output/print_ltac.v                       | 12 ++++++++++++
 5 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 doc/changelog/04-tactics/11203-fix-time-printing.rst
 create mode 100644 test-suite/output/print_ltac.out
 create mode 100644 test-suite/output/print_ltac.v

diff --git a/.gitignore b/.gitignore
index 6c117028a9..7ae2260a86 100644
--- a/.gitignore
+++ b/.gitignore
@@ -92,6 +92,7 @@ test-suite/coqdoc/Coqdoc.*
 test-suite/coqdoc/index.html
 test-suite/coqdoc/coqdoc.css
 test-suite/output/MExtraction.out
+test-suite/output/*.out.real
 test-suite/oUnit-anon.cache
 test-suite/unit-tests/**/*.test
 
diff --git a/doc/changelog/04-tactics/11203-fix-time-printing.rst b/doc/changelog/04-tactics/11203-fix-time-printing.rst
new file mode 100644
index 0000000000..cdfd2b228e
--- /dev/null
+++ b/doc/changelog/04-tactics/11203-fix-time-printing.rst
@@ -0,0 +1,4 @@
+- The optional string argument to :tacn:`time` is now properly quoted
+  under :cmd:`Print Ltac` (`#11203
+  <https://github.com/coq/coq/pull/11203>`_, fixes `#10971
+  <https://github.com/coq/coq/issues/10971>`_, by Jason Gross)
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 ->
diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out
new file mode 100644
index 0000000000..952761acca
--- /dev/null
+++ b/test-suite/output/print_ltac.out
@@ -0,0 +1,8 @@
+Ltac t1 := time "my tactic" idtac
+Ltac t2 := let x := string:("my tactic") in
+           idtac
+           x
+Ltac t3 := idtacstr "my tactic"
+Ltac t4 x := match x with
+             | ?A => (A, A)
+             end
diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v
new file mode 100644
index 0000000000..a992846791
--- /dev/null
+++ b/test-suite/output/print_ltac.v
@@ -0,0 +1,12 @@
+(* Testing of various things about Print Ltac *)
+(* https://github.com/coq/coq/issues/10971 *)
+Ltac t1 := time "my tactic" idtac.
+Print Ltac t1.
+Ltac t2 := let x := string:("my tactic") in idtac x.
+Print Ltac t2.
+Tactic Notation "idtacstr" string(str) := idtac str.
+Ltac t3 := idtacstr "my tactic".
+Print Ltac t3.
+(* https://github.com/coq/coq/issues/9716 *)
+Ltac t4 x := match x with ?A => constr:((A, A)) end.
+Print Ltac t4.
-- 
cgit v1.2.3