The Coq mailing list

[Z <zell08v AT orange.fr>]

Great answers! Thanks a lot for that insight!

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.
*******************

********************
Definition gx(x: nat) := match x with |_ =>0 end.
Eval simpl gx in gx 0.
********************

Here, the issue is that Coq programs that you type are elaborated into a simpler internal language.  For your example, that elaboration includes replacing the [match] with its body, since you have just one pattern that binds no variables.  You can see this by running [Print gx.].

Then, in this case, which tactic to do the unfolding work?

In many contexts, there is no need for unfolding.  For instance:

Goal forall x, gx x = 0.
 reflexivity.
Qed.

This works because at the lowest level of Coq's logic, equality is defined modulo unfolding.  For more complicated cases where you need to massage the form of a goal to get other tactics to apply, you can always run [unfold gx] to unfold [gx] in the conclusion.