From 6759156e7b8234dd4c024d58e63c293c051962f0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 27 Sep 2006 13:14:33 +0000 Subject: [PATCH] New bug found in disambiguation of records. To fix the bug it is necessary to propagate the substitution computed during the type-checking of the constructors to the types of the inductive types. This is quite complex to do. One possibility is simply to add the substitution to the proof status. --- helm/software/matita/tests/record.ma | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/helm/software/matita/tests/record.ma b/helm/software/matita/tests/record.ma index ed9ecfed8..c024acf9e 100644 --- a/helm/software/matita/tests/record.ma +++ b/helm/software/matita/tests/record.ma @@ -37,3 +37,8 @@ record paperino: Prop \def { pippo : paolo \to paolo; piero : True }. + +(* 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 := { f : t A }. -- 2.39.2