]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f11b353) | patch
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
tree04dac74dbdb23b4d42e09d3a3b1f07eb6eca2b90tree | snapshot
parentf11b3533be1310039dd48d0d0e92f96a020bd5e1commit | diff
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 diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.