The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 21/04/2016 17:10, Théo Zimmermann wrote:
> Hello,
> 
> For a goal of the form A /\ B -> C, using intros [] yields the goal A ->
> B -> C (and does not add anything to the context). I would have rather
> expected that A and B be added to the context (this can be achieved with
> intros [] **).
> 
> Is this a wanted behavior? If yes, is it documented somewhere? (I looked
> but did not find any mention of this pattern in the section of the
> manual devoted to intros intro_pattern_list).

See 8.3.2 of the reference manual:

"if the disjunctive pattern is part of a sequence of patterns, then Coq
completes the pattern so that all the arguments of the constructors of
the inductive type are introduced"

which implicitly means that, if the pattern is not part of a sequence
(or rather it is the last one), the arguments are not introduced unless
recursively asked for.

As far as I am concerned, I am fine with this behavior; I dislike it
when Coq invents names in my stead.

Best regards,

Guillaume