diff --git a/CompElliptic/Curves/Pasta.lean b/CompElliptic/Curves/Pasta.lean
index 0bc3185..6d70f1c 100644
--- a/CompElliptic/Curves/Pasta.lean
+++ b/CompElliptic/Curves/Pasta.lean
@@ -113,7 +113,7 @@ example (P : SWPoint curve) : (-1 : ℤ) • P = -P := neg_one_zsmul P
 /-- The Pallas point enumeration, as a computable instantiation of `instFintypeSWPoint`:
 the filter of `F × F` by the decidable `Valid` predicate. Named so the trust census can pin
 its computability. -/
-abbrev fintypePoints : Fintype (SWPoint curve) := inferInstance
+abbrev fintypePoints (_ : Unit) : Fintype (SWPoint curve) := inferInstance
 
 end Pallas
 
@@ -198,7 +198,7 @@ example : OnCurve a b (smul a 3 G) := by native_decide
 /-- The Vesta point enumeration, as a computable instantiation of `instFintypeSWPoint`:
 the filter of `F × F` by the decidable `Valid` predicate. Named so the trust census can pin
 its computability. -/
-abbrev fintypePoints : Fintype (SWPoint curve) := inferInstance
+abbrev fintypePoints (_ : Unit) : Fintype (SWPoint curve) := inferInstance
 
 end Vesta