fix

agda · Jan 30, 2024 · 029d781 · 029d781
1 parent b05276c
commit 029d781
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
@@ -365,7 +365,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
                       (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r))))
         where
         useSolver : ∀ a → a ≡ a · 1r · (1r · 1r)
-        useSolver = solve R'
+        useSolver _ = solve! R'
       pres· (snd (coneOut /1/1Cone (pair i j i<j))) x y =
         cong [_] (≡-× (cong [_] (≡-× refl
                       (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r)))))