diff options
| author | Pierre-Marie Pédrot | 2020-11-02 12:58:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-02 12:58:50 +0100 |
| commit | a392b0225a606b6c8fe0051f0d301d5f3b6d5cd3 (patch) | |
| tree | fb5f0abc2db3c2b21c26b20252f3bb5998626864 /test-suite | |
| parent | 4ab2522244f703f73323ee918bb324cce4b9b237 (diff) | |
| parent | c1e7b28f5977eafd45c36c2ffdca9b7145d867bb (diff) | |
Merge PR #13254: Adopt the same format for "Print Ltac foo" and "Print foo" when "foo" is an Ltac
Reviewed-by: ppedrot
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 |