From 297229e3149f2ea8feba0f5edaa42c7300d63349 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 29 Jul 2023 13:01:39 +0200 Subject: [PATCH] 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). --- theories/Categories/FunctorCategory/Morphisms.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Categories/FunctorCategory/Morphisms.v b/theories/Categories/FunctorCategory/Morphisms.v index e9999aede30..be2cba55ba1 100644 --- 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.