Qualifying idtoiso into Category.Morphisms.idtoiso.

This is to anticipate Coq introducing discharge on the fly and adding new names for discharged constants (see PR #17888).
HoTT · Jul 29, 2023 · 297229e · 297229e
1 parent cca97be
commit 297229e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Categories/FunctorCategory/Morphisms.v b/theories/Categories/FunctorCategory/Morphisms.v
@@ -110,7 +110,7 @@ Section idtoiso.
   Lemma eta_idtoiso
         (F G : object (C -> D))
         (T : F = G)
-  : Morphisms.idtoiso _ T = idtoiso T.
+  : Category.Morphisms.idtoiso _ T = idtoiso T.
   Proof.
     case T.
     expand; f_ap.