]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 05e3a63) | patch
head_beta_reduce used to create applications of applications. Fixed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 10 Jun 2005 11:06:24 +0000 (11:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 10 Jun 2005 11:06:24 +0000 (11:06 +0000)
commit33cb5e3b6c50933f3af870ab66616e034638719d
treec92cd46c3d6a4ddb3816f310dda134a78d646946tree | snapshot
parent05e3a6339cae571d440487a983c78d252d4fb73fcommit | diff
head_beta_reduce used to create applications of applications. Fixed.
head_beta_reduce renamed to beta_reduce (since it performs full beta reduction).
helm/ocaml/cic_omdoc/doubleTypeInference.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.