]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4c2efa4) | patch
New bug found in disambiguation of records.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Sep 2006 13:14:33 +0000 (13:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Sep 2006 13:14:33 +0000 (13:14 +0000)
commit6759156e7b8234dd4c024d58e63c293c051962f0
tree2c881b63acad7c51effff45d74cc0d1ca466c7e9tree | snapshot
parent4c2efa45d1b98541e7a68bb4ef676f5a9788a9ebcommit | diff
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 diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.