+val auto :
+ dbd:HSql.dbd ->
+ params:Auto.auto_params ->
+ universe:Universe.universe -> ProofEngineTypes.tactic
+val cases_intros :
+ ?howmany:int ->
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ ?pattern:ProofEngineTypes.lazy_pattern ->
+ Cic.term -> ProofEngineTypes.tactic