]> matita.cs.unibo.it Git - helm.git/commit
fix universe handling, newly encountered objects are typed in an empty ugraph
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 21 Apr 2008 09:19:23 +0000 (09:19 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 21 Apr 2008 09:19:23 +0000 (09:19 +0000)
commitd120acefa62d997341a84ec54cb1532e223dd661
tree04dac74dbdb23b4d42e09d3a3b1f07eb6eca2b90
parentf11b3533be1310039dd48d0d0e92f96a020bd5e1
fix universe handling, newly encountered objects are typed in an empty ugraph
that after the cleanup phase is committed into the cic_environement and merged
with the current one.

minor reformatting of sources and some more for_all
helm/software/components/cic_proof_checking/cicTypeChecker.ml