* 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
+