]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6b1cb7a) | patch
CProp hierarchy fixed:
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 9 Jul 2008 11:19:02 +0000 (11:19 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 9 Jul 2008 11:19:02 +0000 (11:19 +0000)
commit4d765cc85e3a1e84c80c348a1e67ea1eed984916
tree18df1ebd7e0cf12c57375bb012d426a492f10e95tree | snapshot
parent6b1cb7a439b2e72ec3d6bbb9803e880c82d85020commit | diff
CProp hierarchy fixed:
- CProp universes are not swept away
- CProp i : Type j (where i < j, used to be a fresh j)
- new kernel universe inconsistency error message improved
- pp function for universes constraints for new kernel

Formal topology example fixed to eploit left parameters to reduce the universe
height and solve universe inconsistency
helm/software/components/cic/cicUniv.ml diff | blob | history
helm/software/components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
helm/software/components/cic_proof_checking/cicUnivUtils.ml diff | blob | history
helm/software/components/cic_unification/cicRefine.ml diff | blob | history
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
helm/software/matita/library/demo/formal_topology.ma diff | blob | history
helm/software/matita/library/depends diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.