]> matita.cs.unibo.it Git - helm.git/commit
universes are written with the URI inside objects, this allows
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Apr 2008 15:50:06 +0000 (15:50 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Apr 2008 15:50:06 +0000 (15:50 +0000)
commitc031aa4ca97d0d563a772d7bd247ff7814c51b04
tree83a1bb05480c53e95e3fbaff014d28346007a607
parent6c7be6bbe4e645f5ab99e82d322e1a70503781cb
universes are written with the URI inside objects, this allows
universes to be actually shared between objects and no duplication is necessary.
in this way the typechecker is more strict and unification can be an ungly beast implicitly
adding an = constranint between two universes. speedup granted!
helm/software/components/cic/cicParser.ml
helm/software/components/cic/cicUniv.ml
helm/software/components/cic/cicUniv.mli
helm/software/components/cic_acic/cic2acic.ml
helm/software/components/cic_proof_checking/cicTypeChecker.mli
helm/software/components/library/librarySync.ml