Firstorder_core_plugin.Instancesval collect_quantified :
Environ.env ->
Evd.evar_map ->
Sequent.t ->
Formula.any_formula list * Sequent.tval quantified_tac :
flags:Formula.flags ->
Formula.any_formula list ->
Rules.seqtac Rules.with_backtracking