fix(category_theory/limits/shapes/zero): use fully qualified names in…

… locale (#7619)
leanprover-community · May 20, 2021 · 0cb7ecc · 0cb7ecc
1 parent 5a67f2c
commit 0cb7ecc
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/category_theory/limits/shapes/zero.lean b/src/category_theory/limits/shapes/zero.lean
@@ -177,9 +177,9 @@ This can not be a global instance as it will trigger for every `has_zero C` type
 protected def has_zero : has_zero C :=
 { zero := has_zero_object.zero }
 
-localized "attribute [instance] has_zero_object.has_zero" in zero_object
-localized "attribute [instance] has_zero_object.unique_to" in zero_object
-localized "attribute [instance] has_zero_object.unique_from" in zero_object
+localized "attribute [instance] category_theory.limits.has_zero_object.has_zero" in zero_object
+localized "attribute [instance] category_theory.limits.has_zero_object.unique_to" in zero_object
+localized "attribute [instance] category_theory.limits.has_zero_object.unique_from" in zero_object
 
 @[ext]
 lemma to_zero_ext {X : C} (f g : X ⟶ 0) : f = g :=