/auto_params/.

None, but the tactic may fail finding a proof if every proof is in the search space that is pruned away. Pruning is controlled by the optional params. Moreover, only lemmas whose type signature is a subset of the signature of the current sequent are considered. The signature of a sequent is essentially the set of constats appearing in it.

It closes the current sequent by repeated application of rewriting steps (unless paramodulation is omitted), hypothesis and lemmas in the library.

None