- dbd:HMysql.dbd -> Cic.term option -> Cic.term -> Cic.term option ->
- Cic.name option -> ProofEngineTypes.tactic
+ dbd:HSql.dbd -> automation_cache:AutomationCache.cache ->
+ (string option * Cic.term) option -> Cic.term ->
+ [ `Term of Cic.term | `Auto of Auto.auto_params
+ | `Proof | `SolveWith of Cic.term] ->
+ bool (* last step *) -> ProofEngineTypes.tactic