]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ccbe5c8) | patch
type_of_constant was retunrning the type of the wrong constructor (-1 missing)
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 4 Apr 2008 13:10:22 +0000 (13:10 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 4 Apr 2008 13:10:22 +0000 (13:10 +0000)
commit3ec1830d5251709ed6c4899c74903498a6cd2744
tree99fc01a2c76815b23ea15528c4ab6b503dec765ctree | snapshot
parentccbe5c840923bc9b1a5965f5738c180410ea1df9commit | diff
type_of_constant was retunrning the type of the wrong constructor (-1 missing)
fixpoints were not properly debruijnated before being checked
better error message for match branches
helm/software/components/ng_kernel/nCicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.