The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Is it possible to just add the reimplented refine tactic as a custom
tactic, without too much fuss?

No. At least not as an ltac tactic.

But the code for the new refine is already in v8.4. So you could make a command that runs the new refine. It's sufficient for the case you show, but it can't be combined with other tactics.

If you are familiar with Coq's plugins. The relevant functions are Goal.Refinable.constr_of_raw (or Goal.Refinable.constr_of_open_constr), Goal.refine, Proofview.tclSENSITIVE, and Proof_global.run_tactic  (all of these modules are in the proofs directory).