]> matita.cs.unibo.it Git - helm.git/commitdiff
Does not compile! Wrong unification hint?
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 4 Oct 2009 14:46:18 +0000 (14:46 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 4 Oct 2009 14:46:18 +0000 (14:46 +0000)
helm/software/matita/nlibrary/sets/partitions.ma

index c8898472233191c1dff4cd5a8884e266c5bb527b..80648f4eacddb68f3207b233654d5d7416db18ce 100644 (file)
@@ -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;