Skip to content

Commit 865dfb1

Browse files
fix warning: it was pointing to a record that did not exist. (#2344)
1 parent e72c08e commit 865dfb1

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Algebra/Morphism.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
185185

186186
{-# WARNING_ON_USAGE IsSemigroupMorphism
187187
"Warning: IsSemigroupMorphism was deprecated in v1.5.
188-
Please use IsSemigroupHomomorphism instead."
188+
Please use IsMagmaHomomorphism instead."
189189
#-}
190190
{-# WARNING_ON_USAGE IsMonoidMorphism
191191
"Warning: IsMonoidMorphism was deprecated in v1.5.

0 commit comments

Comments
 (0)