]> matita.cs.unibo.it Git - helm.git/commit
FIXED bug, added assertion in case a universe inside a term T living at URI u
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 11 Apr 2008 15:19:31 +0000 (15:19 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 11 Apr 2008 15:19:31 +0000 (15:19 +0000)
commitb12f894bf4ca947ac868f0fd6bf45ecbb9d84cbe
tree3f1a107ed32578c5a26f476d4d2a336b3a98fc59
parent5cbd03ea1aef33b66c1db22b2de2d9d2f95acb14
FIXED bug, added assertion in case a universe inside a term T living at URI u
was marked with URI v <> u. Unshare.fresh_types should be called!

added a function to linearize a given graph, imperative interface since
is is used only in the new kernel.
helm/software/components/cic/cicUniv.ml
helm/software/components/cic/cicUniv.mli