From e91a64fb380749a3dcbd200d30df0382d89b2a0c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 5 Oct 2014 11:11:48 -0700
Subject: [PATCH] chore(library/logic): fix comments

---
 library/logic/eq.lean         | 2 +-
 library/logic/identities.lean | 2 +-
 library/logic/instances.lean  | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

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