]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c68d980) | 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)
commitfc8f251f8a471249ac6a296c079ccfeb0b535862
tree9c8e78507222bffefc5ef278ef185b81de417b12tree | snapshot
parentc68d9805aa7e37554bc4f00eca61083b75ef43dacommit | 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.
components/cic_proof_checking/cicReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.