Commit 2026-06-11 22:17 0d14bcb8

feat(Tactic): #click_suggestions (#39433) This is an initial PR for a point&click suggestion tool that can suggest theorems and tactics. This PR only implements theorem suggestions. This PR adds the #click_suggestions command that activates the tool. It could potentially in the future be active by default. The code is ported from this repository: https://github.com/JovanGerb/infoview_search A future PR will import this feature in Tactic.Common. We'll have to see if the imports can be minimized for that. This PR deletes unfold? in favour of the #click_suggestions. For backwards compatability, I have left rw?? in place, but I plan to deprecate it in the future.