The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

marco.servetto AT gmail.com
 wrote:
> Hi, I have an (I hope) very simple problem.
> I need a proof that I'm inside some branch of a match case:
> That is, in the following case
> Definition f optA:=
>    match optA with
>      |Some a=>Some ( g a (p:(Some a=optA))
>     |None=>None
>      end.
>
> I need to find the """p""" that have type """Some a=optA"""
> any suggestion?
>    

I assume you're asking about how to define tactics?  If so, the fact 
that you write "Definition" where I would have expected "Ltac" leads me 
to believe that the best way forward may be to read a basic primer on 
Coq tactics.  May I suggest especially Part III of CPDT (though earlier 
parts introduce Ltac basics piecemeal)?
    http://adam.chlipala.net/cpdt/