Dear all,

The `unfold`

tactic only accepts an identifier as input, it does not accept a term, in contrast with the `fold`

tactic. Is there nonetheless a way to unfold the instances of an identifier only when it is applied to a specific value?

A way to do it is of course to unfold all instances, and then fold the ones applied to the other values, but this requires to know the set of possible values.

Some sirens whispered in my ear that it’s out of the box in ssreflect, but this is not an option for me at the moment.

So, would there be a way that I’m unaware of, or a dirty ltac trick, by any chance?

Here is a self-contained, simplified example illustrating the problem:

```
Require Import Program.Basics.
Class Op (A: Type): Type := op: A -> A -> A.
Instance Op_nat: Op nat := plus.
Instance Op_fun {A: Type}: Op (A -> A) := compose.
Goal forall n, op (fun (x:nat) => op x x) (fun (x:nat) => x) n = op (fun (x:nat) => x) (fun (x: nat) => op x x) n.
intros n.
(* Here, I'd like to unfold the occurences of op from the Op_nat instance, but not the others *)
(* However, the following is not supported *)
(* unfold (@op _ Op_nat).*)
(* I _can_ do: *)
unfold op; fold (@op (nat -> nat) Op_fun).
(* But it's quite clearly impractical in general since it requires to know all possible values to which op may be applied, as opposed to exactly the one I want to unfold *)
```

Thanks in advance for any suggestion.

Best,

Yannick