]> matita.cs.unibo.it Git - helm.git/commit
ancient graph regarding universes and trust=false, universes calculated for internal...
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 19 Apr 2008 16:30:21 +0000 (16:30 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 19 Apr 2008 16:30:21 +0000 (16:30 +0000)
commite8f4be1c4c7d4162035dd45ac4ea38b9ed168098
treea6304b2371d12107bb1105ecb6533a1a6498cb28
parentefc3d154e69c0fb18215901f5c4de3a73ebc2fb5
ancient graph regarding universes and trust=false, universes calculated for internal objects
were used for the toplevel object (that should be sound) but cleaned using the univ list of
the internal object
helm/software/components/cic_proof_checking/cicTypeChecker.ml