X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.mli;h=b53e506914552d50f949cecd38364823d3a4b2b8;hb=4d765cc85e3a1e84c80c348a1e67ea1eed984916;hp=fd501df8c47c4adfa320d90151ebc07b47c89e74;hpb=b12f894bf4ca947ac868f0fd6bf45ecbb9d84cbe;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index fd501df8c..b53e50691 100644
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -66,13 +66,13 @@ val oblivion_ugraph: universe_graph
   UniverseInconsistency
 *)
 val add_eq: 
-  ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+  universe -> universe -> universe_graph -> universe_graph
 val add_ge: 
-  ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+  universe -> universe -> universe_graph -> universe_graph
 val add_gt: 
-  ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+  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
@@ -152,10 +153,4 @@ val assert_univ: universe -> unit
 val compare: universe -> universe -> int
 val eq: universe -> universe -> bool
 
-(*
-  Benchmarking stuff
-*)
-val get_spent_time: unit -> float
-val reset_spent_time: unit -> unit
-
 val is_anon: universe -> bool