The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

Adam Chlipala wrote:
> (I'm not entirely sure if [intro] really does head normalization.  It 
> might use some other, similar reduction strategy.)

You are correct, intro does not quite do head normalization: if the goal is 
not an explicit product or let-in, intro repeatedly tries to apply the "red" 
reduction tactic, which tries to unfold the head constant and then reduces 
all apparent head beta/iota/zeta redexes (reducing manifest applications of 
fun/fix, match-withs and let-ins, when possible).
  This is almost the same as doing head normalization, except if you goal 
happens to be something like an explcit beta redex, in which case red does 
nothing (try it!) and intro fails miserably. This does not happen too often 
in fully interactive use because most high-level tactics have an epilogue 
that beta-iota normalizes the goal, but does occur rather annoyingly this 
when you start using more tacticals.

  Georges