]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 48e3181) | patch
New: cache of translated fixpoints (to avoid the generative fix restriction and
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 10 Apr 2008 18:14:47 +0000 (18:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 10 Apr 2008 18:14:47 +0000 (18:14 +0000)
commit7c3850896b6324306bdbe8ef430f500cc9cb7f83
tree9f75fd80ead414d9ae4b3f33a6ecd554ffea7584tree | snapshot
parent48e318104379fb77181c88e83afc5c4814aaba99commit | diff
New: cache of translated fixpoints (to avoid the generative fix restriction and
to avoid pollution of the environment). Many more Matita objects now pass.

TODO: the caching machinery should be debugged and better understood (what about
metasenv and subst?)
helm/software/components/ng_kernel/Makefile diff | blob | history
helm/software/components/ng_kernel/alluris.txt diff | blob | history
helm/software/components/ng_kernel/oCic2NCic.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.