I’m trying to have a succinct notation for defining instances using a tactic. However, it seems that defining instances this way may cause a significant slowdown. I’m afraid a self-contained example will be hard to extract, but my situation is similar to the following:

```
Class C (arg : Prop) :=
class_def : arg -> arg. (* some complicated prop dependent on arg *)
Ltac solve := unfold C; intros a; exact a. (* some expensive tactic *)
Instance holds1 : C True := ltac:(solve). (* takes 3 minutes for the actual instance *)
Definition holds2 : C True := ltac:(solve). (* takes 25 seconds .. *)
Instance holds3 : C True. Proof. solve. Defined. (* takes 25 seconds .. *)
Instance holds4 : C True. Proof. solve. Qed. (* takes 25 seconds .. *)
```

Does anyone have an idea what might cause this? I would expect that at least `holds1`

and `holds2`

take the same amount of time.