]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f5e4a6c) | patch
guarded_by_constructors implemented, some cleanup here and there.
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 May 2008 13:34:10 +0000 (13:34 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 May 2008 13:34:10 +0000 (13:34 +0000)
commitbace52692eba06fca2cc37857b61dadf5d280ffe
tree16f488fa509e870e7dd1d4e9ba50af63bf6e09f6tree | snapshot
parentf5e4a6c59a95c7f78e36924bce433abf8d59bf87commit | diff
guarded_by_constructors implemented, some cleanup here and there.
fix_lefts_in_constr fixed: the inductive type list was returned with
constructors instantiated and debruijned, but with types whose arity was
instantiated with lefts too. This is wrong since we want to use these types to
build a context, that is closed, and will be put at the end of the actual
context since debruijn will make uris point to those terms
helm/software/components/ng_kernel/nCicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.