Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
val main: HMysql.dbd ->
bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
+val demodulate_tac:
+ dbd:HMysql.dbd ->
+ pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic