X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteTypes.mli;h=b26c0ca21fb6e13bf408dbaf6f06fd54fd6fba0e;hb=6ada20fa68668e9d23842767fe643efc04f9d29a;hp=a8b86c27639fc9fe0f678332c7c1c94aeb4f5e1f;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index a8b86c276..b26c0ca21 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/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