The status has been extended with a "universe", that is a

[helm.git] / components / grafite_engine / grafiteTypes.mli

diff --git a/components/grafite_engine/grafiteTypes.mli b/components/grafite_engine/grafiteTypes.mli
index a8b86c27639fc9fe0f678332c7c1c94aeb4f5e1f..b26c0ca21fb6e13bf408dbaf6f06fd54fd6fba0e 100644 (file)
--- 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