]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5cbd03e) | patch
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
tree3f1a107ed32578c5a26f476d4d2a336b3a98fc59tree | snapshot
parent5cbd03ea1aef33b66c1db22b2de2d9d2f95acb14commit | diff
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 diff | blob | history
helm/software/components/cic/cicUniv.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.