X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.mli;h=8a24614c2a814482838d09be95c148ebd179d52a;hb=04f22df647f35080b499b720bca7bc0eb1794c64;hp=b53e506914552d50f949cecd38364823d3a4b2b8;hpb=832269bdc098f021af72619c5f5c7547c0121770;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index b53e50691..8a24614c2 100644
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -60,6 +60,10 @@ val empty_ugraph: universe_graph
 (* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
 val oblivion_ugraph: universe_graph
 
+(* one of the previous two, no set to empty_ugraph *)
+val default_ugraph: universe_graph
+
+
 (*
   These are the real functions to add eq/ge/gt constraints 
   to the passed graph, returning an updated graph or raising
@@ -72,7 +76,7 @@ val add_ge:
 val add_gt: 
   universe -> universe -> universe_graph -> universe_graph
 
-val do_rank: universe_graph -> int list
+val do_rank: universe_graph -> int list * universe list
 val get_rank: universe -> int
 
 (*