fix #guard_msgs output

Author: kim-em

MathlibTest/GCongr/GCongr.lean

@@ -48,7 +48,7 @@ a b c d : ℕ
 h : b~d
 ⊢ a~a
 
-case a.a
+case a
 a b c d : ℕ
 h : b~d
 ⊢ c~c

MathlibTest/GRewrite.lean

@@ -215,7 +215,7 @@ the inequality goes in the wrong direction). -/
 /--
 error: Tactic `grewrite` failed: could not discharge x ≤ y using x ≥ y
 
-case h₁.hbc
+case hbc
 x y b : ℚ
 h : x ≥ y
 ⊢ x ≤ y
@@ -257,7 +257,7 @@ example {Prime : ℕ → Prop} {a a' : ℕ} (h₁ : Prime (a + 1)) (h₂ : a = a
 /--
 error: Tactic `grewrite` failed: could not discharge b ≤ a using a ≤ b
 
-case h₂.hbc
+case hbc
 a b c : ℚ
 h₁ : a ≤ b
 h₂ : 0 ≤ c

MathlibTest/Linarith/Basic.lean

@@ -728,7 +728,6 @@ example (x : ℤ) : 0 ≤ x * wrapped x := by nlinarith
 def tightlyWrapped (z : ℤ) : ℤ := z
 /--
 error: linarith failed to find a contradiction
-case h
 x : ℤ
 a✝ : x * tightlyWrapped x < 0
 ⊢ False

MathlibTest/congr.lean

@@ -332,7 +332,6 @@ example (inst1 : BEq α) [LawfulBEq α] (inst2 : BEq α) [LawfulBEq α] (xs : Li
 
 /--
 error: unsolved goals
-case h.e'_2
 α : Type
 inst1 : BEq α
 inst✝¹ : LawfulBEq α

MathlibTest/conv_widget.lean

@@ -83,8 +83,7 @@ conv =>
     enter [1, x, 5]
     skip
 ---
-trace: case h
-x : False
+trace: x : False
 | true
 -/
 #guard_msgs in
@@ -115,8 +114,7 @@ conv =>
     enter [1, 0, x, 1]
     skip
 ---
-trace: case h
-x : Unit
+trace: x : Unit
 | false
 -/
 #guard_msgs in
@@ -384,8 +382,7 @@ conv =>
     enter [1, 0, x0, x1, x2, 2]
     skip
 ---
-trace: case h.h.h
-x0 x1 x2 : Bool → Nat
+trace: x0 x1 x2 : Bool → Nat
 | x2 true
 -/
 #guard_msgs in