new tactics are almost ready

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

diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 244ce615f67f01542759a7a2cc1ecf23dc2a53e1..aa90dc0e0194951ae1f87f711ef3c4994b7d7806 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -51,6 +51,7 @@ type status = {
   coercions: CoercDb.coerc_db;
   universe:Universe.universe;  
   baseuri: string;
+  ng_status: NTactics.tac_status option;
 }
 
 let get_current_proof status =