The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Georgi Guninski wrote:
> I have problem using a Lemma as a coercion.
>
> Trying this, get stuck on goal "coer a" and can't compute/unfold it:
>
>
> (* Definition coer := fun a:True =>  Prop. *)
> Lemma coer: True->Prop.
> intro. exact True.
> Qed.
>    

End in [Defined] instead of [Qed], which makes the definition 
transparent instead of opaque.  This particular example would be much 
clearer as:
    Definition coer (_ : True) := True.
though perhaps your real example is more involved, to the point where 
tactics are called for.  Personally, I recommend never using tactics to 
define a term with computationally significant behavior.