The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 17/08/2013 14:32, t x wrote:
> (1) construct existentials using tactics or
> (2) have some form of rewrite generate new goals rather than existentials?

Have you tried the refine tactic? You give it a partial term 
corresponding to the part of the proof you're building, and it turns the 
holes into goals.

To simulate a rewrite, you have to refine a term on [eq_rect], like this 
for instance:

Goal forall m n, m + S n = S (m + n).
Proof.
intros m n.
refine (eq_rect _ _ _ _ (plus_Sn_m _ _)).
Abort.

PMP