]> matita.cs.unibo.it Git - helm.git/commit
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
tree18df1ebd7e0cf12c57375bb012d426a492f10e95
parent6b1cb7a439b2e72ec3d6bbb9803e880c82d85020
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
helm/software/components/cic_proof_checking/cicTypeChecker.ml
helm/software/components/cic_proof_checking/cicUnivUtils.ml
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/ng_kernel/check.ml
helm/software/components/ng_kernel/nCicEnvironment.ml
helm/software/components/ng_kernel/nCicEnvironment.mli
helm/software/matita/library/demo/formal_topology.ma
helm/software/matita/library/depends