The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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.