]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 68f93b8) | patch
End of patch for computation of LetIn types. Now types of mutually (co)recursive
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 20 Mar 2008 09:23:30 +0000 (09:23 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 20 Mar 2008 09:23:30 +0000 (09:23 +0000)
commit44b1f0c3a1e4bdc0abc3b02004c7b385ab63f7c5
tree2c4c915342694d4789fb8c1402bf7303b090b331tree | snapshot
parent68f93b859c6b978bfd66c03fb383985f835f6657commit | diff
End of patch for computation of LetIn types. Now types of mutually (co)recursive
function are added to the environment _after_ Implicit have been resolved.
helm/software/components/cic/deannotate.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.