Abstract over select occurrences of a term

Stream: general

[Jannis Limperg]

I'd like to have a tactic that takes an expression e and replaces some term s with t in e (like kabstract etc.) -- but only at certain locations within e. (Or, alternatively, everywhere in e except for certain 'blocked' locations.) Is this already a thing?

Example: Given the term x + x, I want to be able to say, "replace the first x but not the second."

[Gabriel Ebner]

I often use conv in ... { rw ... } for this.

[Mario Carneiro]

I think you can also use rw [] {occurrences := ...} for this

[Jannis Limperg]

Thanks! I'm not sure whether I'll be able to make rewrite-based tactics work for my particular problem, but I'll try.

[Alex J. Best]

You can make a lot of tactics into conv tactics, like ring and simp, this might fit your paradigm?