?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
-(* The default callback always decomposes the term as much as possible *)
val decompose_tac:
- ?uris_choice_callback:
- ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list ->
- (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
- Cic.term ->
- ProofEngineTypes.tactic
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ ?user_types:((UriManager.uri * int) list) ->
+ dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic