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
---
 test-suite/output/print_ltac.out |  8 ++++++++
 test-suite/output/print_ltac.v   | 12 ++++++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 test-suite/output/print_ltac.out
 create mode 100644 test-suite/output/print_ltac.v

(limited to 'test-suite')

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