Bug fixing. If the inductive types do not occur in t, t is

[helm.git] / matita / tests / TPTP / unit_equality_problems.txt

diff --git a/matita/tests/TPTP/unit_equality_problems.txt b/matita/tests/TPTP/unit_equality_problems.txt
index c394ddd956fbebb3fabab2bf63eb32b5bf70f66a..c296865bdc03d6b8a670d78eaf21391d55abde7d 100644 (file)
--- a/matita/tests/TPTP/unit_equality_problems.txt
+++ b/matita/tests/TPTP/unit_equality_problems.txt
@@ -99,14 +99,6 @@ COL002-1
 COL002-4
 COL002-5
 COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
 COL003-2
 COL004-1
 COL004-3
@@ -199,8 +191,6 @@ COL064-6
 COL064-7
 COL064-8
 COL064-9
-COL064-1
-COL064-1
 COL065-1
 COL066-1
 COL066-2