]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 397b5f9) | patch
Convertibility now converts machines in place of terms.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jul 2007 17:54:40 +0000 (17:54 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jul 2007 17:54:40 +0000 (17:54 +0000)
commit72206bee39e35bcc5cf8a7074ade13a4a81c0c08
tree6fc731be5d1aaedac56a58c1372d01ec19eb3c12tree | snapshot
parent397b5f9d848e63a9703a1f90faf9869092ec8893commit | diff
Convertibility now converts machines in place of terms.
Actually, the heads of the machines (i.e. everything but the stack) are
still unwinded and converted as terms. Thus there is much space for
improvement.
helm/software/components/cic_proof_checking/cicReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.