fix(algebra/*/colimits): avoid explicit infer_instance (#1430)

With an explicit universe level Lean can do it automatically.
leanprover-community · Sep 11, 2019 · 8a5156f · 8a5156f
1 parent 45fe081
commit 8a5156f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/src/algebra/CommRing/colimits.lean b/src/algebra/CommRing/colimits.lean
@@ -427,8 +427,7 @@ def colimit_is_colimit : is_colimit (colimit_cocone F) :=
     refl
   end }.
 
--- FIXME why is this infer_instance needed!?
-instance has_colimits_CommRing : @has_colimits CommRing.{v} infer_instance :=
+instance has_colimits_CommRing : has_colimits.{v} CommRing.{v} :=
 { has_colimits_of_shape := λ J 𝒥,
   { has_colimit := λ F, by exactI
     { cocone := colimit_cocone F,

diff --git a/src/algebra/Mon/colimits.lean b/src/algebra/Mon/colimits.lean
@@ -231,8 +231,7 @@ def colimit_is_colimit : is_colimit (colimit_cocone F) :=
     refl
   end }.
 
--- FIXME why is this infer_instance needed!?
-instance has_colimits_Mon : @has_colimits Mon.{v} infer_instance :=
+instance has_colimits_Mon : has_colimits.{v} Mon.{v} :=
 { has_colimits_of_shape := λ J 𝒥,
   { has_colimit := λ F, by exactI
     { cocone := colimit_cocone F,