-val saturate :
- HMysql.dbd ->
- ?full:bool ->
- ?depth:int ->
- ?width:int ->
- ProofEngineTypes.proof * ProofEngineTypes.goal ->
- (UriManager.uri option * Cic.conjecture list * Cic.term * Cic.term) *
- 'a list
+val reset_refs : unit -> unit
+
+val make_active: Equality.equality list -> active_table
+val make_passive: Equality.equality list -> passive_table
+val add_to_passive: Equality.equality list -> passive_table -> passive_table
+val list_of_passive: passive_table -> Equality.equality list
+
+val simplify_equalities :
+ Equality.equality_bag ->
+ UriManager.uri ->
+ Utils.environment ->
+ Equality.equality list ->
+ Equality.equality list
+val pump_actives :
+ Cic.context ->
+ Equality.equality_bag ->
+ int ->
+ active_table ->
+ passive_table ->
+ int ->
+ float ->
+ active_table * passive_table * int
+val all_subsumed :
+ Equality.equality_bag ->
+ int ->
+ ProofEngineTypes.status ->
+ active_table ->
+ passive_table ->
+ (Cic.substitution *
+ ProofEngineTypes.proof *
+ ProofEngineTypes.goal list) list * int
+val given_clause:
+ Equality.equality_bag ->
+ int -> (* maxmeta *)
+ ProofEngineTypes.status ->
+ active_table ->
+ passive_table ->
+ int -> int -> float ->
+ (Cic.substitution *
+ ProofEngineTypes.proof *
+ ProofEngineTypes.goal list) option *
+ active_table * passive_table * int