From 536c87d73cef9b92a75d9c24ed63cfb821d3e893 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 2 Jun 2025 14:27:22 +0200 Subject: [PATCH] chore: make test more robust --- tests/lean/run/invalid_dotted_identifier_prop.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/lean/run/invalid_dotted_identifier_prop.lean b/tests/lean/run/invalid_dotted_identifier_prop.lean index f702152ee2..2faf44251d 100644 --- a/tests/lean/run/invalid_dotted_identifier_prop.lean +++ b/tests/lean/run/invalid_dotted_identifier_prop.lean @@ -8,9 +8,10 @@ def foo (n : Nat) : Nat := | .true => n | .false => 47 +set_option pp.mvars.anonymous false in /-- error: Invalid dotted identifier notation: not supported on type - Sort ?u.44 + Sort _ -/ #guard_msgs in def foo2 (n : Nat) : Nat :=