]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fac7052) | patch
better error message, functions to clear various caches used during translation of...
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 12 Dec 2008 12:08:16 +0000 (12:08 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 12 Dec 2008 12:08:16 +0000 (12:08 +0000)
commit3f551aa5900d5c756eb48cea751c032b3bcbcf37
treebaee164755903cdd858d8b0ecec60d71717416actree | snapshot
parentfac7052d076fbfe531dd95aa57d8ec2381f23648commit | diff
better error message, functions to clear various caches used during translation of old2new cic, logger functions implemented inside the typechecker so that
uncommenting one line makes the type checker more verbose when recursively typing stuff
helm/software/components/ng_kernel/nCicLibrary.ml diff | blob | history
helm/software/components/ng_kernel/nCicLibrary.mli diff | blob | history
helm/software/components/ng_kernel/nCicTypeChecker.ml diff | blob | history
helm/software/components/ng_kernel/oCic2NCic.ml diff | blob | history
helm/software/components/ng_kernel/oCic2NCic.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.