The Coq mailing list

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

On 03/07/2013 20:28, t x wrote:
> To me, this seems easier to debug -- in that suppose I fail to solve the
> goal. Then, in T1, I end up having an extra goal (and when dealing with
> large proofs with 20 subgoal and handling them in parappel, it's not
> obvious to me where it's coming from. In T2, hopefully I get an type error
> directly at Command1 because I couldn't provide the term.

I if understand correctly, you want to be sure to solve the generated 
goal. To this intent, you may use the [solve] tacticial. This gives:

refine ((fun (H0 : _statement_) => _ (lemma ... H0 ...)) _);
[ | solve[_tactic_] ].

Is that what you want ?

PMP