X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautomationCache.mli;h=8b032870f128951e3d591f832317825ae09f8b76;hb=23f2fafa1bd91f271c0b5cf982b1cc59dc74cc35;hp=00fb516e238efd4bfbc381fba83373fb1315624b;hpb=b4f6b1a39b59e923527f5c17d8fdd0fa1e13e1bf;p=helm.git

diff --git a/helm/software/components/tactics/automationCache.mli b/helm/software/components/tactics/automationCache.mli
index 00fb516e2..8b032870f 100644
--- 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
+