The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

> I second Cedric's answer, you should try refine or Program. Note that
> there is probably a nicer way to do wha
Sorry, premature sending :)

So I was saying, unless this is really what you want to do, you should
maybe try and rethink what you're doing in order to avoid mixing
definitions and proofs.
A final note: you can use refine and still have proofs opaque, by
using the abstract tactic: abstract (<tactic>) applies tactic, which
should solve the current goal, and saves it as an opaque lemma. The
downside is you need to prove every subgoal in one tactic, or one
chain of tactic. If you have trouble with that particular point, ask
Adam Chlipala :)

S.
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06