The Coq mailing list

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

Make sure you have decent alternatives for all current uses of
"instantiate" before your sense of elegance takes over.  Thanks in
advance.

I doubt it's reasonable to even consider removing [instantiate] from Ltac in the foreseeable future. I didn't mean to imply it would be. My hope is, rather, that better solutions will be found with the new mechanism. I must say that you are right, though: [erewrite] is rather thorny.