From d1f4f68c3cd7162e8b86e5ae3a27eb0250fb8095 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 Nov 2024 22:29:45 +1100 Subject: [PATCH] fix test --- MathlibTest/Simps.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MathlibTest/Simps.lean b/MathlibTest/Simps.lean index 8def1aa96d6ef..2c3e0d2f69483 100644 --- a/MathlibTest/Simps.lean +++ b/MathlibTest/Simps.lean @@ -1203,7 +1203,7 @@ structure Foo where @[simps field field_2 field_9_fst] def myFoo : Foo := ⟨1, ⟨1, 1⟩, 1⟩ -structure Prod (X Y : Type _) extends Prod X Y +structure Prod (X Y : Type _) extends _root_.Prod X Y structure Prod2 (X Y : Type _) extends Prod X Y