The Coq mailing list

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

Cool!  These tactics need to be dressed up a bit using Tactic Notation.  But, now I think I can deal with the possible deprecation of instantiate.

Nice tactics. But to reiterate: instantiate is not getting deprecated. It is just somewhat encouraged to seek other means of dealing with existential variables, especially by using the new dependent subgoal feature (which is, unfortunately not pervasive in existing, so it may not always be possible, like in Xavier's [erewrite] example above). So there's nothing to be afraid of, really.