The Coq mailing list

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

> But beware, I am not sure you can make parts of this program opaque and
> other transparents; that means that your term will either be unfoldable
> everywhere with its full proof (when terminating with "Defined")
> or never unfoldable (when terminating with "Qed"),
> but to produce an unfoldable skeleton with opaque proofs, I am pretty
> sure that you need "Program".

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

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