From 7433f1b6439e7c5eb532546b533980686636f468 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Oct 2009 14:46:18 +0000 Subject: [PATCH] Does not compile! Wrong unification hint? --- helm/software/matita/nlibrary/sets/partitions.ma | 9 --------- 1 file changed, 9 deletions(-) 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; -- 2.39.2