A better rapply?

[JasonGross]

We should consider consolidating erapply and rapply into a single tactic without an argument length limit, as @jonleivent recently suggested on coqdev:

Tactic Notation "is_valid_open_constr" uconstr(term) :=
  try tryif (refine (let _ := term in _)) then fail else fail 1 term "is not a valid open_constr".

Tactic Notation "rapply" uconstr(term) :=
  let rec f t :=
    tryif (refine t)
    then idtac
    else tryif is_valid_open_constr (t _)
         then f uconstr:(t _)
         else fail 0 term "cannot be applied" in f term.

uconstr has all-around better behavior, I believe; it will not try to infer typeclasses before it knows the type of the goal, nor insert evars where inference can be done.

[Alizter]

Is this still possible? I would be in favour of something like this.

[JasonGross]

The code looks like it should just work; try it and see if it works, and submit a PR or report on the results?

[mikeshulman]

Is there a version of this code that works with our new do_with_holes?

[JasonGross]

We should probably use a version that doesn't do eager typeclass resolution (either take the one from Coq: https://github.com/coq/coq/blob/a0b92c67a1d2d45d45f0d482a3303b7416153d67/theories/Program/Tactics.v#L175-L179, or else relaxed the refine-test with an open_constr test in is_valid_open_constr). But, yes, we should just be able to use something like this in place of do_with_holes, I believe.