The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Z wrote:
> For your 2nd point
> "we don't need unfold explicitely..."
> which I take leave to doubt however:
>
> For the following theorem, is there another way to
> get around? (without unfold)
>
> *****************
> Definition gxx(x: nat) := match x with |_ =>0 end.
> Theorem test000bis: gxx 0 = 0.
> Proof. unfold gxx. Qed.
> *******************

Yes.  Like I said before, [reflexivity] proves this theorem directly.