Module `Firstorder_plugin.Instances`

val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.any_formula list * Sequent.t
val quantified_tac : flags:Formula.flags -> Formula.any_formula list -> Rules.seqtac Rules.with_backtracking