diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index 636b119a55..760394d975 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -3,7 +3,7 @@
 -- Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 import .prop
 
--- logic.connectives.eq
+-- logic.eq
 -- ====================
 
 -- Equality.
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index d5f48b79e4..61e8ea4c00 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -6,7 +6,7 @@
 -- ============================
 
 -- Useful logical identities. In the absence of propositional extensionality, some of the
--- calculations use the type class support provided by logic.connectives.instances
+-- calculations use the type class support provided by logic.instances
 
 import logic.instances logic.decidable logic.quantifiers logic.cast
 
diff --git a/library/logic/instances.lean b/library/logic/instances.lean
index 6c991d10e8..5d92f55a33 100644
--- a/library/logic/instances.lean
+++ b/library/logic/instances.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 
--- logic.core.instances
+-- logic.instances
 -- ====================
 
 import logic.connectives algebra.relation