]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c48c7e2) | patch
lefts_and_tys was tys@lefts, CSC claims it was working since that context is only...
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 Apr 2008 11:55:43 +0000 (11:55 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 Apr 2008 11:55:43 +0000 (11:55 +0000)
commit26b754bcd3763fd7624637adab0635edefa1168f
tree70d20d2a552c3bc0043937a866daf859c1787629tree | snapshot
parentc48c7e28f54e00e12755f703a8c46187be701ed2commit | diff
lefts_and_tys was tys@lefts, CSC claims it was working since that context is only used
by whd and it did not contain any definitions by contructions, thus the length was the only important bit
helm/software/components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.