From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 4 Oct 2009 14:46:18 +0000 (+0000)
Subject: Does not compile! Wrong unification hint?
X-Git-Tag: make_still_working~3387
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7433f1b6439e7c5eb532546b533980686636f468;p=helm.git

Does not compile! Wrong unification hint?
---

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index c88984722..80648f4ea 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -19,15 +19,6 @@ include "nat/minus.ma".
 include "datatypes/pairs.ma".
 
 alias symbol "eq" = "setoid eq".
-
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: ext_powerclass support;