X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Fcoercions.ma;h=337ef50edc1fc2a63bb1600e0ca6f0f32dc005f8;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=8a45f29295d067744e28346312b7fd5558393f60;hpb=0dbd5619f82e575948ba583317706b4e794f57eb;p=helm.git

diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma
index 8a45f2929..337ef50ed 100644
--- a/helm/matita/tests/coercions.ma
+++ b/helm/matita/tests/coercions.ma
@@ -29,10 +29,3 @@ alias symbol "eq" (instance 0) = "leibnitz's equality".
 theorem a: fst O one = fst (positive O) (next one).
 reflexivity.
 qed.
-
-
-
-
-
-
-