Merge PR #11203: Make the string argument of `time` print correctly

Ack-by: Zimmi48
Reviewed-by: ppedrot

2 files changed, 20 insertions, 0 deletions

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.