X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoCache.mli;h=c4c99c3821c2b8d70506542233fed3a752f27f10;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=b47a29925ca322f13867afe4533a8948f7755ac2;hpb=2eaee49a7ff3ed74598a0db84ce4dbc5bca92380;p=helm.git

diff --git a/helm/software/components/tactics/autoCache.mli b/helm/software/components/tactics/autoCache.mli
index b47a29925..c4c99c382 100644
--- a/helm/software/components/tactics/autoCache.mli
+++ b/helm/software/components/tactics/autoCache.mli
@@ -31,16 +31,14 @@ type cache_elem =
   | UnderInspection
   | Notfound
 val get_candidates: cache -> Cic.term -> Cic.term list
-val cache_add_library: 
-  HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list ->
-    cache -> cache
-val cache_add_context: Cic.context -> Cic.metasenv -> cache -> cache
-
+val cache_add_list: 
+    cache -> Cic.context -> (Cic.term*Cic.term) list -> cache
 val cache_examine: cache -> cache_key -> cache_elem
 val cache_add_failure: cache -> cache_key -> int -> cache 
 val cache_add_success: cache -> cache_key -> Cic.term -> cache
 val cache_add_underinspection: cache -> cache_key -> int -> cache
 val cache_remove_underinspection: cache -> cache_key -> cache
+val cache_reset_underinspection: cache -> cache
 val cache_empty: cache
 val cache_print: Cic.context -> cache -> string
 val cache_size: cache -> int