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