From 3305480bb0ed6ba527f772f9dfbb1f51960a9a3d Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 3 Apr 2024 21:18:27 -0400 Subject: [PATCH] fix warning: it was pointing to a record that did not exist. --- src/Algebra/Morphism.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda index 45b7a46a1d..e3bcb53e9b 100644 --- a/src/Algebra/Morphism.agda +++ b/src/Algebra/Morphism.agda @@ -185,7 +185,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂} {-# WARNING_ON_USAGE IsSemigroupMorphism "Warning: IsSemigroupMorphism was deprecated in v1.5. -Please use IsSemigroupHomomorphism instead." +Please use IsMagmaHomomorphism instead." #-} {-# WARNING_ON_USAGE IsMonoidMorphism "Warning: IsMonoidMorphism was deprecated in v1.5.