- ?user_types:(UriManager.uri * int) list ->
- dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic
-val demodulate :
- dbd:HMysql.dbd ->
- pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
-val discriminate : term:Cic.term -> ProofEngineTypes.tactic
+ ?user_types:(UriManager.uri * int option) list ->
+ ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
+val demodulate : dbd:HMysql.dbd ->
+ universe:Universe.universe -> ProofEngineTypes.tactic
+val destruct : term:Cic.term -> ProofEngineTypes.tactic