X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_engine%2FgrafiteTypes.mli;h=b26c0ca21fb6e13bf408dbaf6f06fd54fd6fba0e;hb=67cf4ce16c346991c8eda71576414f5c6324ab82;hp=a8b86c27639fc9fe0f678332c7c1c94aeb4f5e1f;hpb=54bd25811bc80555936eebaf95b137857f6db06a;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