The Coq mailing list

[Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>]

Hi!

I'm new to Ltac and I'm trying to define a tactic that will take a hypothesis 
name as an argument, match the formula/type of this hypothesis and then do 
something with the parts that have been matched.

Here is a concrete minimal (and kind-of dumb-looking) example of the kind of 
tactic I would like to write:

Ltac my_and_elimination H H0 := match goal with
     | [ H: ?A /\ ?B |- _ ] => assert (H0: A); let H1:=fresh in let H2:=fresh 
in destruct H as [H1 H2]; exact H1
end.






I know this is wrong (it doesn't behave as expected in my proof scripts). The 
question is: how could I do it correctly? 

Best regards,

Bruno