The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

On 04/21/2016 05:34 PM, Guillaume Melquiond wrote:
> 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
> 

Of course you can force the behavior you want with

intros [ ? ? ].

Dominique