new tactics are almost ready

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

diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index 95f65f3601c84d63ca53b533d57700a1da7623f7..3a833f6da056bb029915a80f204234670f8473e3 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/components/grafite_engine/grafiteTypes.mli
@@ -49,6 +49,7 @@ type status = {
   coercions: CoercDb.coerc_db;
   universe:Universe.universe;  (** universe of terms used by auto *)
   baseuri: string;
+  ng_status: NTactics.tac_status option;
 }
 
 val dump_status : status -> unit