* http://helm.cs.unibo.it/
*)
+(* Cic.Type of universe *)
type universe
+
+(* returns a fresh universe and puts it in the working graph *)
val fresh: unit -> universe
+
+(* add eq/ge/gt constraints to the woring graph *)
val add_eq: universe -> universe -> bool
val add_ge: universe -> universe -> bool
val add_gt: universe -> universe -> bool
-(*
-val string_of_universe: universe -> string
-val print_map: unit -> unit
-*)
+(* prints the graphs *)
+val print_global_graph: unit -> unit
+val print_working_graph: unit -> unit
+
+type universe_graph
+val get_working: unit -> universe_graph
+val set_working: universe_graph -> unit
+
+val directly_to_env_begin: unit -> unit
+val directly_to_env_end: unit -> unit
-val reset: unit -> unit
+val reset_working: unit -> unit
-(* val check_status_eq: universe list -> bool *)