[Feature Request] Project-wide advanced refactoring.

[pseudohuman92]

I would like to see some project-wide advanced refactoring support. I am using IntelliJ for my Java projects and its refactoring mechanism makes everything neater and much more well defined.

Couple of things that can immensely help clearing up codebase:

• When you change the name of a definition, theorem, tactic etc. it automatically goes thru all project files and changes the places that it is used. It would be even better if it is scope aware. For example if I have

File1.v
Definition foo := something.

File2.v
Definition foo := something else.

If I change File2 foo to bar, it should change only the files that uses File2's foo

• Shifting H references in a portion of a code / proof by 1 forward/backward

Sometimes, during or after a proof. I add a premise to the theorem or add/remove an extra clause to a definition. This causes most of the sentences in the context to shift by 1. Then I have to go through the proof script and edit every single of them by hand.

• Finding common proof script portions.

Most of the time, first I finish a proof without creating many lemmas / tactics, then go through the script to identify recurring goals and turn them into lemmas and/or tactics. If extension could identify similar looking proof script portions, That would make it much easier to detect such recurring portions in the proof.

[gares]

I flag this as for the new document manager which will hopefully have support for some code actions