]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 832269b) | patch
The code for universes was not correct in many borderline cases.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 17 May 2008 11:14:46 +0000 (11:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 17 May 2008 11:14:46 +0000 (11:14 +0000)
commitb5f64556ec797a92c2c79d9d1c6aefa4dcf880b1
tree18d3dd68548fe18cc67ceecd6518ef02d4fa57a7tree | snapshot
parent832269bdc098f021af72619c5f5c7547c0121770commit | diff
The code for universes was not correct in many borderline cases.
The new code should be correct. For sure, it is much simpler, shorter,
characterized by better invariants and its interface has less functions.
helm/software/components/ng_kernel/check.ml diff | blob | history
helm/software/components/ng_kernel/nCicEnvironment.ml diff | blob | history
helm/software/components/ng_kernel/nCicEnvironment.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.