]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7d6f47c) | patch
get_check_fix and cofix unified, bug regarding debruijnation of constructors types...
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 May 2008 17:02:26 +0000 (17:02 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 May 2008 17:02:26 +0000 (17:02 +0000)
commit659d8c3d93c3279e08bc0cf56879037e066d9ca8
tree33181d3a95c0d32512b3a2aeb41f04b805e42235tree | snapshot
parent7d6f47c980081e06fee46c08d5b5bd7faf1e6aa9commit | diff
get_check_fix and cofix unified, bug regarding debruijnation of constructors types fixed everywhere.
the constructor typs are debruinated wrt some inductive type uri an not wrt
their own, thus a wrong context was created. guarded by constructors ported from the old kernel.
helm/software/components/ng_kernel/nCicEnvironment.ml diff | blob | history
helm/software/components/ng_kernel/nCicEnvironment.mli diff | blob | history
helm/software/components/ng_kernel/nCicReduction.ml diff | blob | history
helm/software/components/ng_kernel/nCicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.