fix: what did I just push??

Author: HoshinoTented

Diff for: cli-impl/src/test/resources/negative/GoalAndMeta.txt

@@ -190,15 +190,6 @@ Error: Unable to solve the type of this literal:
 Let's learn from that.
 
 NonPattern:
-In file C:\Users\hoshino\Documents\Projects\project-aya\aya-dev\cli-impl\src\test\resources\shared\src\data\vec\base.aya:5:6 ->
-
-  3 │   open inductive Vec (n : Nat) (A : Type) elim n
-  4 │   | 0 => []
-  5 │   | suc n => infixr :> A (Vec n A)
-    │         ╰╯
-
-Warning: The name `n` shadows a previous local definition from outer scope
-
 In file $FILE:9:3 ->
 
   6 │       def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)

Diff for: cli-impl/src/test/resources/negative/PatTyckError.txt

@@ -13,15 +13,6 @@ Error: Unknown constructor
 Let's learn from that.
 
 SelectionFailed:
-In file C:\Users\hoshino\Documents\Projects\project-aya\aya-dev\cli-impl\src\test\resources\shared\src\data\vec\base.aya:5:6 ->
-
-  3 │   open inductive Vec (n : Nat) (A : Type) elim n
-  4 │   | 0 => []
-  5 │   | suc n => infixr :> A (Vec n A)
-    │         ╰╯
-
-Warning: The name `n` shadows a previous local definition from outer scope
-
 In file $FILE:4:2 ->
 
   2 │   open import data::vec::base
@@ -46,7 +37,7 @@ Error: I'm unsure if there should be a case for
        as index unification is blocked for type
          Vec (<n> + <n>) A
 
-2 error(s), 1 warning(s).
+2 error(s), 0 warning(s).
 Let's learn from that.
 
 SelectionBlocked: