]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5b26547) | patch
Fixed serious bug that occurred only in the following situation:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 9 Apr 2008 14:57:34 +0000 (14:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 9 Apr 2008 14:57:34 +0000 (14:57 +0000)
commitbf4f7d923f1bcf1f07d5d4f46fc6f8e7bce4b578
tree04b4950fbae10dc5c7e063a3ab85014be674c9c6tree | snapshot
parent5b265471ff8da58400656f4899e8a2f398e8a2adcommit | diff
Fixed serious bug that occurred only in the following situation:

\lambda x.
Fix f {
\lambda y: P x.
Fix g {

The two fixes must be translated as

Fix f { \lambda x. \lambda y: P x. ...}
Fix g { \lambda x. \lambda f. \lambda y: P x. ... }

In the first case, the x that occurs in the type of y must be a Rel 1.
In the second case, the x that occurs in the type of y must be a Rel 2.
The previous code translated both of them to Rel 1.
helm/software/components/ng_kernel/oCic2NCic.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.