Avoid other comparisons on universes using =.

[helm.git] / helm / software / components / cic / cicUniv.mli

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index 7a4331905b50ea95689302c90135011e5649ec5d..7b422583f53f361da3e247fb5717ac313eb7f70c 100644 (file)
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -66,11 +66,14 @@ 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 get_rank: universe -> int
 
 (*
   debug function to print the graph to standard error
@@ -149,9 +152,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