]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5159ebf) | 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)
commitae1827aaba945a25bdc209ca23aa836befa4bead
tree8e8ccf10134577f4219de51c0da628d2aef5858btree | snapshot
parent5159ebf165bfc5015612cf8ce112ba89e68617bccommit | 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.
matita/tests/record.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.