3 files changed, 10 insertions, 1 deletions
diff --git a/test-suite/output/bug_13004.out b/test-suite/output/bug_13004.out
new file mode 100644
index 0000000000..2bd7d67535
--- /dev/null
+++ b/test-suite/output/bug_13004.out
@@ -0,0 +1,2 @@
+Ltac bug_13004.t := ltac2:(print (of_string "hi"))
+Ltac bug_13004.u := ident:(H)
diff --git a/test-suite/output/bug_13004.v b/test-suite/output/bug_13004.v
new file mode 100644
index 0000000000..bf4a8285d0
--- /dev/null
+++ b/test-suite/output/bug_13004.v
@@ -0,0 +1,7 @@
+Require Import Ltac2.Ltac2 Ltac2.Message.
+
+Ltac t := ltac2:(print (of_string "hi")).
+Ltac u := ident:(H).
+
+Print t.
+Print u.
diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out
index 58931c4b82..5f88ec2e41 100644
--- a/test-suite/output/print_ltac.out
+++ b/test-suite/output/print_ltac.out
@@ -4,7 +4,7 @@ Ltac t2 := let x := string:("my tactic") in
            x
 Ltac t3 := idtacstr "my tactic"
 Ltac t4 x := match x with
-             | ?A => (A, A)
+             | ?A => constr:((A, A))
              end
 The command has indeed failed with message:
 idnat is bound to a notation that does not denote a reference.