Test/Metavar.lean

@@ -192,7 +192,7 @@ def test_proposition_generation: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "?m.29 x"])
+    #[.some "?m.30 x"])
   addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
   let assign := "Eq.refl x"

Test/Tactic/MotivatedApply.lean

@@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
 
     addTest $ ← conduit.withContext do
       let t := toString (← Meta.ppExpr $ ← conduit.getType)
-      return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
+      return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.150 ?m.{majorId}) = (n + 0 = n)")
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [