X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_engine%2FgrafiteTypes.mli;h=b26c0ca21fb6e13bf408dbaf6f06fd54fd6fba0e;hb=24dd4569daf1d35bffaa813b8164058d8643f14d;hp=a8b86c27639fc9fe0f678332c7c1c94aeb4f5e1f;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/grafite_engine/grafiteTypes.mli b/components/grafite_engine/grafiteTypes.mli
index a8b86c276..b26c0ca21 100644
--- a/components/grafite_engine/grafiteTypes.mli
+++ b/components/grafite_engine/grafiteTypes.mli
@@ -53,7 +53,8 @@ type status = {
   proof_status: proof_status;                             (** logical status *)
   options: options;
   objects: UriManager.uri list;  (** in-scope objects *)
-  coercions: UriManager.uri list;                      (** defined coercions *)
+  coercions: UriManager.uri list; (** defined coercions *)
+  universe:Universe.universe;  (** universe of terms used by auto *)
 }
 
 val dump_status : status -> unit