fix

leanprover-community · Apr 13, 2023 · a3c7e4e · a3c7e4e
1 parent ec47359
commit a3c7e4e
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -388,6 +388,5 @@ end
 
 end ModuleCat
 
-@[nolint dangerousInstance]
-instance (M : Type u) [AddCommGroup M] [Module R M] : Coe (Submodule R M) (ModuleCat R) :=
+instance (M : Type u) [AddCommGroup M] [Module R M] : CoeOut (Submodule R M) (ModuleCat R) :=
   ⟨fun N => ModuleCat.of R N⟩