val saturate :
+ bool ->
HMysql.dbd ->
?full:bool ->
?depth:int ->
Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
val main: HMysql.dbd ->
bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
-val demodulate_tac:
- dbd:HMysql.dbd ->
- pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val demodulate_tac: dbd:HMysql.dbd -> ProofEngineTypes.tactic
val superposition_tac:
- what:string -> other:string -> subterms_only:bool ->
- demodulate:bool ->
- ProofEngineTypes.proof * ProofEngineTypes.goal ->
+ target:string -> table:string -> subterms_only:bool ->
+ demod_table:string -> ProofEngineTypes.proof * ProofEngineTypes.goal ->
ProofEngineTypes.proof * ProofEngineTypes.goal list
val get_stats: unit -> string