- init_cache_and_tables rewritten using the automation_cache

[helm.git] / helm / software / components / tactics / automationCache.mli

diff --git a/helm/software/components/tactics/automationCache.mli b/helm/software/components/tactics/automationCache.mli
index 00fb516e238efd4bfbc381fba83373fb1315624b..8b032870f128951e3d591f832317825ae09f8b76 100644 (file)
--- a/helm/software/components/tactics/automationCache.mli
+++ b/helm/software/components/tactics/automationCache.mli
@@ -23,11 +23,22 @@
  * http://cs.unibo.it/helm/.
  *)
 
+type tables = 
+  Saturation.active_table * Saturation.passive_table * Equality.equality_bag
+
 type cache = {
         univ : Universe.universe;
-        tables : Saturation.active_table * Saturation.passive_table;
+        tables : tables;
 }
 
 
-val empty : cache
+val empty_tables : unit -> tables
+val empty : unit -> cache
+
+val add_term_to_active: 
+  cache -> Cic.metasenv -> Cic.substitution -> Cic.context -> 
+    Cic.term -> Cic.term option -> cache
+val pump: cache -> int -> cache
+val pp_cache: cache -> unit
+