X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUniv.mli;h=f98ea84c6ce411e6541cd9179c93332ecad25ef2;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=d7eb7dc413e9bb6e460b3cd645f09dd2e07e2485;hpb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;p=helm.git

diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli
index d7eb7dc41..f98ea84c6 100644
--- 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 *)