- dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
-val destruct : Cic.term option -> ProofEngineTypes.tactic
+ dbd:HSql.dbd ->
+ params:Auto.auto_params ->
+ automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic
+val destruct : Cic.term list option -> ProofEngineTypes.tactic