]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e8efcf3) | patch
Tentative (and bad!) fix of outtypes in non-dependent eliminations.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 7 Apr 2008 23:16:36 +0000 (23:16 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 7 Apr 2008 23:16:36 +0000 (23:16 +0000)
commitd7fd52648af0f0d0dc8ca53c5582281531973243
tree4c826113ccb1109e75f1ddd2af600e261992e0ectree | snapshot
parente8efcf326c54299f3c758eb8f96cd80251833b90commit | diff
Tentative (and bad!) fix of outtypes in non-dependent eliminations.
The fix does not work since there is no guarantee in Coq that the outtype
is made of a sequence of Lambdas (and indeed it is not for automatically
generated elimiantion principles). Thus I need to perform recursion on the
type of the outtype and I also need to perform some eta-expansion to insert
the additional lambda in the right position :-(
helm/software/components/ng_kernel/oCic2NCic.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.