The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Jeffrey Terrell wrote:
> I'd be grateful if someone could tell me why
>
> Definition P : Prop := True -> True -> True.
> Goal P.
> intro.
>
> unfolds P (and adds True to the context) whereas
>
> Definition P : Prop := True -> True -> True.
> Goal P.
> intros.
>
> doesn't.

[intro] is defined to head-normalize the goal before proceeding, while 
[intros] works directly with the syntax it's given.  Among other 
properties, head-normalization is guaranteed to result in a term that is 
an implication, if the input term is definitionally equivalent to some 
implication.

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