The Coq mailing list

[Z <zell08v AT orange.fr>]

Here is another example that I have some trouble to understand, where simpl. does not want to unfold gx although it should have considered that "match"

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

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

Thank you.
Zell

   [simpl] only unfolds definitions when doing so causes some [match]
   to simplify.  I hope it's not hard to see the consequences of this
   heuristic for the two examples, and why it leads to the [simpl]
   behavior you see.