The Coq mailing list

[Ben Moseley <ben_moseley AT mac.com>]

Thanks Adam.

(I see now that this issue is mentioned in Section 12.3 of your book...)

--Ben

On 25 Nov 2010, at 19:57, Adam Chlipala wrote:

> Ben Moseley wrote:
>>   match goal with | [ |- context [match ?d with
>>                                     | Some _ =>  (match ?y with
>>                                                    | Left  =>  true
>>                                                    | Right =>  true
>>                                                  end)
>>                                     | None =>  true
>>                                   end] ] =>  destruct d; [|reflexivity]
>>   end.
>> 
>> ... then the match fails.
>> 
>> If instead I replace the '?y' with '_', then it succeeds.
>>   
> 
> A term bound to a simple Ltac pattern variable isn't allowed to contain 
> locally-bound variables.  The locally-bound variable that causes the 
> trouble in this example is what you're writing as [_] for the [Some] 
> pattern.
> 
> Conversely, a [_] pattern may match terms containing local variables, since 
> there's no need to produce a version of the matched term that can be 
> dropped into other contexts.