chore(MathlibTest): prefer setting pp.mvars.anonymous to false over pp.mvars (leanprover-community#34604)

The new option only replaces autogenerated anonymous metavariables,
but leaves ordinary accessible mvars with names present.

Author: grunweg

MathlibTest/Algebra/MonoidAlgebra/Defs.lean

@@ -4,7 +4,7 @@ variable {R M A} [Semiring R] [Monoid M] [AddMonoid A]
 section Notation
 open scoped MonoidAlgebra AddMonoidAlgebra
 
-set_option pp.mvars false
+set_option pp.mvars.anonymous false
 -- TODO: could resolve ambiguity based on Monoid / AddMonoid
 /--
 error: Ambiguous term

MathlibTest/EuclideanSpace.lean

@@ -10,7 +10,7 @@ section delaborator
 #guard_msgs in
 #check !₂[1, 2, 3]
 
-set_option pp.mvars false in
+set_option pp.mvars.anonymous false in
 /-- info: !₀[] : WithLp 0 (Fin 0 → ?_) -/
 #guard_msgs in
 #check !₀[]

MathlibTest/FinCoercions.lean

@@ -5,7 +5,7 @@
 
 import Mathlib
 
-set_option pp.mvars false
+set_option pp.mvars.anonymous false
 
 -- We first verify that there is no global coercion from `Nat` to `Fin n`.
 -- Such a coercion would frequently introduce unexpected modular arithmetic.

MathlibTest/Util/PrintSorries.lean

@@ -1,6 +1,6 @@
 import Mathlib.Util.PrintSorries
 
-set_option pp.mvars false
+set_option pp.mvars.anonymous false
 
 /-!
 Direct use of `sorry`

MathlibTest/abel.lean

@@ -179,7 +179,7 @@ h : R (2 • myId x) (2 • myId x)
 ⊢ True
 -/
 #guard_msgs (trace) in
-set_option pp.mvars false in
+set_option pp.mvars.anonymous false in
 example (x : ℤ) (R : ℤ → ℤ → Prop) (hR : Reflexive R) : True := by
   have h : R (myId x + x) (x + myId x) := hR ..
   abel_nf at h

MathlibTest/conv_widget.lean

@@ -154,7 +154,7 @@ example : 1 = Nat.log2 4 → False := by
   test "/0/1/1"
   exact test_sorry
 
-set_option pp.mvars false in
+set_option pp.mvars.anonymous false in
 /--
 info: `conv?` would output:
 conv =>

MathlibTest/superscript.lean

@@ -194,7 +194,7 @@ open Nat' (γ) in
 #guard_msgs in #check testsub(ᵧ ₙ)
 
 /- The delaborator should reject metavariables. -/
-set_option pp.mvars false in
+set_option pp.mvars.anonymous false in
 /-- info: checkSubscript ?_ : Unit -/
 #guard_msgs in #check checkSubscript ?_