diff --git a/library/data/bool.lean b/library/data/bool.lean
index 6dab8d81a..d6aca2af4 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.connectives.basic logic.classes.decidable logic.classes.inhabited
+import logic.core.connectives logic.classes.decidable logic.classes.inhabited
 
 using eq_ops decidable
 
diff --git a/library/data/option.lean b/library/data/option.lean
index 7aee37087..580c75837 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.connectives.basic logic.connectives.eq logic.classes.inhabited logic.classes.decidable
+import logic.core.eq logic.classes.inhabited logic.classes.decidable
 using eq_ops decidable
 
 namespace option
diff --git a/library/data/prod.lean b/library/data/prod.lean
index 8dd06edf1..3821e7cc7 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -7,7 +7,7 @@
 
 -- The cartesian product.
 
-import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
+import logic.classes.inhabited logic.core.eq logic.classes.decidable
 
 using inhabited decidable
 
diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index cd8830701..4606c0bcd 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -5,8 +5,8 @@
 -- Theory data.quotient
 -- ====================
 
-import logic tools.tactic ..subtype logic.connectives.cast struc.relation data.prod
-import logic.connectives.instances
+import logic tools.tactic ..subtype logic.core.cast struc.relation data.prod
+import logic.core.instances
 import .aux
 
 using relation prod inhabited nonempty tactic eq_ops
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 948808c42..4e901fc77 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.classes.inhabited logic.connectives.eq
+import logic.classes.inhabited logic.core.eq
 
 using inhabited
 
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index 0a30c05b1..ffd7103e0 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
+import logic.classes.inhabited logic.core.eq logic.classes.decidable
 
 using decidable
 
diff --git a/library/data/sum.lean b/library/data/sum.lean
index e2f6bf107..111bc023a 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -7,7 +7,7 @@
 
 -- The sum type, aka disjoint union.
 
-import logic.connectives.prop logic.classes.inhabited logic.classes.decidable
+import logic.core.prop logic.classes.inhabited logic.classes.decidable
 
 using inhabited decidable
 
@@ -81,4 +81,4 @@ rec_on s1
         show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
       (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
 
-end sum
\ No newline at end of file
+end sum
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index 8295503b5..04b1787f9 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -1,10 +1,8 @@
-----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-----------------------------------------------------------------------------------------------------
 
-import logic.connectives.basic logic.connectives.quantifiers logic.connectives.cast struc.relation
+import logic.core.quantifiers logic.core.cast struc.relation
 
 using eq_ops
 
diff --git a/library/logic/axioms/funext.lean b/library/logic/axioms/funext.lean
index 79ce0419d..86dfcef8a 100644
--- a/library/logic/axioms/funext.lean
+++ b/library/logic/axioms/funext.lean
@@ -4,7 +4,7 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import logic.connectives.eq struc.function
+import logic.core.eq struc.function
 using function
 
 -- Function extensionality
diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean
index 1f4c9ab90..e62bb72d1 100644
--- a/library/logic/axioms/hilbert.lean
+++ b/library/logic/axioms/hilbert.lean
@@ -8,7 +8,7 @@
 -- Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the
 -- constructive one).
 
-import logic.connectives.eq logic.connectives.quantifiers
+import logic.core.quantifiers
 import logic.classes.inhabited logic.classes.nonempty
 import data.subtype data.sum
 
diff --git a/library/logic/axioms/piext.lean b/library/logic/axioms/piext.lean
index b9fb633a7..de74d159c 100644
--- a/library/logic/axioms/piext.lean
+++ b/library/logic/axioms/piext.lean
@@ -4,7 +4,7 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import logic.classes.inhabited logic.connectives.cast
+import logic.classes.inhabited logic.core.cast
 
 using inhabited
 
diff --git a/library/logic/classes/decidable.lean b/library/logic/classes/decidable.lean
index 9f9629b15..5015d1d85 100644
--- a/library/logic/classes/decidable.lean
+++ b/library/logic/classes/decidable.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.connectives.basic logic.connectives.eq
+import logic.core.connectives
 
 namespace decidable
 
diff --git a/library/logic/classes/inhabited.lean b/library/logic/classes/inhabited.lean
index 2c8cf3cc5..ebd994e98 100644
--- a/library/logic/classes/inhabited.lean
+++ b/library/logic/classes/inhabited.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import logic.connectives.basic
+import logic.core.connectives
 
 inductive inhabited (A : Type) : Type :=
 inhabited_mk : A → inhabited A
diff --git a/library/logic/classes/nonempty.lean b/library/logic/classes/nonempty.lean
index b11fdc021..3a446b825 100644
--- a/library/logic/classes/nonempty.lean
+++ b/library/logic/classes/nonempty.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import logic.connectives.basic .inhabited
+import .inhabited
 
 using inhabited
 
diff --git a/library/logic/connectives/cast.lean b/library/logic/core/cast.lean
similarity index 100%
rename from library/logic/connectives/cast.lean
rename to library/logic/core/cast.lean
diff --git a/library/logic/connectives/basic.lean b/library/logic/core/connectives.lean
similarity index 100%
rename from library/logic/connectives/basic.lean
rename to library/logic/core/connectives.lean
diff --git a/library/logic/connectives/connectives.md b/library/logic/core/core.md
similarity index 88%
rename from library/logic/connectives/connectives.md
rename to library/logic/core/core.md
index 1aaa8380d..d4558a5b9 100644
--- a/library/logic/connectives/connectives.md
+++ b/library/logic/core/core.md
@@ -4,8 +4,8 @@ logic.connectives
 Logical operations and connectives.
 
 * [prop](prop.lean) : the type Prop
-* [basic](basic.lean) : propositional connectives
 * [eq](eq.lean) : equality and disequality
+* [connectives](connectives.lean) : propositional connectives
 * [cast](cast.lean) : casts and heterogeneous equality
 * [quantifiers](quantifiers.lean) : existential and universal quantifiers
 * [if](if.lean) : if-then-else
diff --git a/library/logic/connectives/eq.lean b/library/logic/core/eq.lean
similarity index 100%
rename from library/logic/connectives/eq.lean
rename to library/logic/core/eq.lean
diff --git a/library/logic/connectives/examples/examples.md b/library/logic/core/examples/examples.md
similarity index 100%
rename from library/logic/connectives/examples/examples.md
rename to library/logic/core/examples/examples.md
diff --git a/library/logic/connectives/examples/instances_test.lean b/library/logic/core/examples/instances_test.lean
similarity index 100%
rename from library/logic/connectives/examples/instances_test.lean
rename to library/logic/core/examples/instances_test.lean
diff --git a/library/logic/connectives/identities.lean b/library/logic/core/identities.lean
similarity index 90%
rename from library/logic/connectives/identities.lean
rename to library/logic/core/identities.lean
index 330d9e23d..e76336253 100644
--- a/library/logic/connectives/identities.lean
+++ b/library/logic/core/identities.lean
@@ -8,13 +8,10 @@
 -- Useful logical identities. In the absence of propositional extensionality, some of the
 -- calculations use the type class support provided by logic.connectives.instances
 
-import logic.connectives.instances
+import logic.core.instances
 
 using relation
 
--- TODO: delete when calc bug is fixed
-calc_subst subst_iff
-
 theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
 calc
   (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _
@@ -38,6 +35,3 @@ calc
   a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff_symm (and_assoc _ _ _)
     ... ↔ (b ∧ a) ∧ c : {and_comm a b}
      ... ↔ b ∧ (a ∧ c) : and_assoc _ _ _
-
--- TODO: delete when calc bug is fixed
-calc_subst subst
diff --git a/library/logic/connectives/if.lean b/library/logic/core/if.lean
similarity index 100%
rename from library/logic/connectives/if.lean
rename to library/logic/core/if.lean
diff --git a/library/logic/connectives/instances.lean b/library/logic/core/instances.lean
similarity index 98%
rename from library/logic/connectives/instances.lean
rename to library/logic/core/instances.lean
index 9184cd28c..cb12d0ff0 100644
--- a/library/logic/connectives/instances.lean
+++ b/library/logic/core/instances.lean
@@ -2,7 +2,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 
-import logic.connectives.basic logic.connectives.eq struc.relation
+import logic.core.connectives struc.relation
 
 namespace relation
 
diff --git a/library/logic/connectives/prop.lean b/library/logic/core/prop.lean
similarity index 100%
rename from library/logic/connectives/prop.lean
rename to library/logic/core/prop.lean
diff --git a/library/logic/connectives/quantifiers.lean b/library/logic/core/quantifiers.lean
similarity index 98%
rename from library/logic/connectives/quantifiers.lean
rename to library/logic/core/quantifiers.lean
index 3bb489122..6f7239eee 100644
--- a/library/logic/connectives/quantifiers.lean
+++ b/library/logic/core/quantifiers.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import .basic .eq ..classes.nonempty
+import .connectives ..classes.nonempty
 
 using inhabited nonempty
 
diff --git a/library/logic/default.lean b/library/logic/default.lean
index b71c7a420..73eef2c39 100644
--- a/library/logic/default.lean
+++ b/library/logic/default.lean
@@ -2,8 +2,8 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 
-import logic.connectives.basic logic.connectives.eq logic.connectives.cast 
-import logic.connectives.quantifiers logic.connectives.if 
+import logic.core.connectives logic.core.eq logic.core.cast 
+import logic.core.quantifiers logic.core.if 
 import logic.classes.decidable logic.classes.inhabited logic.classes.nonempty
-import logic.connectives.instances
-import logic.connectives.identities
\ No newline at end of file
+import logic.core.instances
+import logic.core.identities
diff --git a/library/logic/logic.md b/library/logic/logic.md
index 9386ca6bb..815ae19ec 100644
--- a/library/logic/logic.md
+++ b/library/logic/logic.md
@@ -4,7 +4,7 @@ logic
 Logical constructions and axioms. By default, `import logic` does not
 import any additional axioms.
 
-* [connectives](connectives/connectives.md) : logical connectives
+* [core](core/core.md) : logical connectives
 * [axioms](axioms/axioms.md) : additional axioms
 * [classes](classes/classes.md) : classes for inhabited types, 
 decidable types, etc.  
diff --git a/library/struc/binary.lean b/library/struc/binary.lean
index d6ab7c484..f6755aa0a 100644
--- a/library/struc/binary.lean
+++ b/library/struc/binary.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.connectives.eq
+import logic.core.eq
 using eq_ops
 
 namespace binary
diff --git a/library/struc/relation.lean b/library/struc/relation.lean
index eed8f0174..f2d2b151f 100644
--- a/library/struc/relation.lean
+++ b/library/struc/relation.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 
-import logic.connectives.prop
+import logic.core.prop
 
 
 -- General properties of relations
diff --git a/library/struc/struc.md b/library/struc/struc.md
index a100096df..63be3cc70 100644
--- a/library/struc/struc.md
+++ b/library/struc/struc.md
@@ -6,5 +6,4 @@ Axiomatic properties and structures.
 * [function](function.lean)
 * [relation](relation.lean)
 * [binary](binary.lean) : binary operations
-* [equivalence](equivalence.lean) : equivalence relations
 * [wf](wf.lean) : well-founded relations
diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean
index fb4d5dbc8..8e054488b 100644
--- a/tests/lean/run/congr_imp_bug.lean
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -3,7 +3,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
-import logic.connectives.basic struc.function
+import logic.core.connectives struc.function
 using function
 
 namespace congr
@@ -44,4 +44,4 @@ theorem congr_and_comp [instance] {T : Type} {R : T → T → Prop} {f1 f2 : T 
      (C1 : struc R iff f1) (C2 : struc R iff f2) :
    congr.struc R iff (λx, f1 x ∧ f2 x) := congr.compose21 congr_and C1 C2
 
-end congr
\ No newline at end of file
+end congr
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index 03e50fb86..c34f0c300 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.connectives.prop logic.classes.inhabited logic.classes.decidable
+import logic.core.prop logic.classes.inhabited logic.classes.decidable
 
 using inhabited decidable
 
@@ -67,4 +67,4 @@ rec_on s1
         show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
       (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
 
-end sum
\ No newline at end of file
+end sum