new universes implementation

[helm.git] / helm / ocaml / cic / cicUniv.mli

diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli
index d7eb7dc413e9bb6e460b3cd645f09dd2e07e2485..f98ea84c6ce411e6541cd9179c93332ecad25ef2 100644 (file)
--- a/helm/ocaml/cic/cicUniv.mli
+++ b/helm/ocaml/cic/cicUniv.mli
@@ -23,17 +23,27 @@
  * 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 *)