X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.mli;h=b53e506914552d50f949cecd38364823d3a4b2b8;hb=4d765cc85e3a1e84c80c348a1e67ea1eed984916;hp=7b422583f53f361da3e247fb5717ac313eb7f70c;hpb=5cd2efd21063b304c30a9486a562bdff7852957b;p=helm.git diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli index 7b422583f..b53e50691 100644 --- a/helm/software/components/cic/cicUniv.mli +++ b/helm/software/components/cic/cicUniv.mli @@ -72,7 +72,7 @@ val add_ge: val add_gt: universe -> universe -> universe_graph -> universe_graph -val do_rank: universe_graph -> unit +val do_rank: universe_graph -> int list val get_rank: universe -> int (* @@ -133,6 +133,7 @@ val restart_numbering: returns the universe number (used to save it do xml) *) val univno: universe -> int +val univuri: universe -> UriManager.uri (** re-hash-cons URIs contained in the given universe so that phisicaly * equality could be enforced. Mainly used by