From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 15 Oct 2007 11:32:46 +0000 (+0000)
Subject: Wrong test patched.
X-Git-Tag: 0.4.95@7852~118
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=808e0ec0ecef2cb14939f4f05724d36663495f40;p=helm.git

Wrong test patched.
---

diff --git a/matita/tests/record.ma b/matita/tests/record.ma
index 1c73c8951..bc5d2e217 100644
--- a/matita/tests/record.ma
+++ b/matita/tests/record.ma
@@ -41,4 +41,4 @@ record paperino: Prop \def {
 (* the following test used to show the following bug: the left
    parameter A in the type of t was not unified with the left
    parameter A in the type of the constructor of the record *)
-record t (A:Type) : Type := { f : t A }.
+record t (A:Type) : Type := { f : A }.
\ No newline at end of file