I am having a strange case where this works

```
match goal with H: of_slot_data d ≡ ps |- _ => rename H into H1 end.
```

but when I try to wrap this code into a tactic, it fails

```
Tactic Notation "myrename" uconstr(pat) "into" ident(Hnew) :=
lazymatch goal with| H : pat |- _ => rename H into Hnew end.
```

I tried `uconstr`

, `open_constr`

and `constr`

, all to no avail. I think what happens is that when I call my own tactic, Coq infers the term to be

```
@equiv (cmra_car per_slot) (ofe_equiv (cmra_ofeO per_slot)) (of_slot_data d) ps
```

which does not match the hypothesis any more. However, when I write a `match`

inline in the proof script it works, possibly because it defers inferring the hole (the type of the equivalence).

is there any way to actually abstract over the pattern of a `match`

?

(btw, `open_constr`

seems not listed at https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation)

I can't contribute anything to the problem, and likely this is unrelated, but it should be `into Hnew`

, not `into Hew`

in your `myrename`

oh, so maybe I was mislead by that typo during my experiments

but we have `rename select pat into name`

in std++ and that one also fails, so it's not *just* me being silly^^

yeah it still fails the same way after fixing that

`Set Ltac Debug`

shows that it does not even enter the match arm; it's the `lazymatch`

that breaks

I think you're hitting the famous pattern_of_constr piece of code.

yeah, I think I might

and it's entirely unnecessary, all I really need is `Tactic Notation "mytac" pattern(foo)`

Any updates on this? I end up using this which is not ideal

```
Tactic Notation "rename_by_type" constr(t) "into" ident(Hname) :=
match goal with
| H : context [t] |- _ => rename H into Hname
end.
```

I was about to ask this exactly same question but the search lead me to here, I was trying this

```
(* this works *)
Tactic Notation "when" uconstr(x) "do" tactic(t) :=
match goal with
| |- context[x] => t
| _ => idtac
end.
(* this not *)
Tactic Notation "apply_by_type" uconstr(t) :=
match goal with
| H' : t |- _ => apply H'
end.
Variable a : Set.
Variable P : a -> Prop.
Variable Q : Prop.
Axiom PQ : forall x, P x -> Q.
Goal forall x, (P x) -> Q.
intros ?.
when (P _ -> _) do (apply PQ).
Qed.
Goal forall x, P x -> P x.
intros ? ?.
(* this fails *)
Fail apply_by_type (P x).
(* but this works *)
match goal with
| H : P _ |- _ => apply H
end.
Qed.
```

@Daniel Hilst Selli for a slight improvement see here https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v#L651

That still has the bug that Ralf described, but in somewhat advanced scenarios; that tactic mostly works

thanks @Paolo Giarrusso

BTW this file is a perl of ltac, lots of rich examples

Last updated: Jun 15 2024 at 05:01 UTC