]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (from: 6759156)
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)
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.


No differences found
Unnamed repository; edit this file 'description' to name the repository.