diff options
| author | Hugo Herbelin | 2020-10-22 18:57:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-29 14:36:28 +0100 |
| commit | c1e7b28f5977eafd45c36c2ffdca9b7145d867bb (patch) | |
| tree | 982d7c792cf51ddced0792e97e26ab288ee0f3cd /test-suite | |
| parent | 473160ebe4a835dde50d6c209ab17c7e1b84979c (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/bug_13004.out | 4 | ||||
| -rw-r--r-- | test-suite/output/bug_13238.out | 8 |
2 files changed, 6 insertions, 6 deletions
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 |