X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Flogic%2Fequality.ma;h=a5d2f0d1e461cd5c02e95aa5f2eb1ec04f96d5fd;hb=aeb7f0539398561dc84cadf38df14a051dd1ba75;hp=84f7df2e66144c8a90a74a757af063c9b674709f;hpb=b86d8020e759afa1adcb8fe3571eeac288edfd83;p=helm.git

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 84f7df2e6..a5d2f0d1e 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -15,7 +15,6 @@
 set "baseuri" "cic:/matita/logic/equality/".
 
 include "higher_order_defs/relations.ma".
-include "logic/connectives.ma".
 
 inductive eq (A:Type) (x:A) : A \to Prop \def
     refl_eq : eq A x x.