]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: efc3d15) | patch
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
treea6304b2371d12107bb1105ecb6533a1a6498cb28tree | snapshot
parentefc3d154e69c0fb18215901f5c4de3a73ebc2fb5commit | diff
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 diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.