From c1e7b28f5977eafd45c36c2ffdca9b7145d867bb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2020 18:57:10 +0200
Subject: Use same code for "Print Ltac foo" and "Print foo" when "foo" is an
 Ltac.

Adopting the same format means printing "Ltac foo := ..." and not the
fully qualified name of foo.
---
 test-suite/output/bug_13004.out | 4 ++--
 test-suite/output/bug_13238.out | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/bug_13004.out b/test-suite/output/bug_13004.out
index 2bd7d67535..28bc580202 100644
--- a/test-suite/output/bug_13004.out
+++ b/test-suite/output/bug_13004.out
@@ -1,2 +1,2 @@
-Ltac bug_13004.t := ltac2:(print (of_string "hi"))
-Ltac bug_13004.u := ident:(H)
+Ltac t := ltac2:(print (of_string "hi"))
+Ltac u := ident:(H)
diff --git a/test-suite/output/bug_13238.out b/test-suite/output/bug_13238.out
index bda21aa9e3..a17d05200d 100644
--- a/test-suite/output/bug_13238.out
+++ b/test-suite/output/bug_13238.out
@@ -1,4 +1,4 @@
-Ltac bug_13238.t1 x := replace (x x) with (x x)
-Ltac bug_13238.t2 x := case : x 
-Ltac bug_13238.t3 := by move ->
-Ltac bug_13238.t4 := congr True 
+Ltac t1 x := replace (x x) with (x x)
+Ltac t2 x := case : x 
+Ltac t3 := by move ->
+Ltac t4 := congr True 
-- 
cgit v1.2.3