a. uniform mangement for context and library

[helm.git] / components / tactics / autoCache.mli

diff --git a/components/tactics/autoCache.mli b/components/tactics/autoCache.mli
index b47a29925ca322f13867afe4533a8948f7755ac2..61c658811fec86dd1934c632c40949c35a736fa2 100644 (file)
--- a/components/tactics/autoCache.mli
+++ b/components/tactics/autoCache.mli
@@ -31,11 +31,8 @@ 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