The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

On 10/30/2013 12:59 PM, Bruno Woltzenlogel Paleo wrote:
> 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 am not sure you can directly match the name of an assumption. One way 
to do it is

Ltac my_and_elimination H name :=
  let A :=
    match type of H with
    ?A /\ ?B  =>  A
    end in
    assert (name : A).

Goal True /\ False -> False.
intros H.
my_and_elimination H B.
admit.