CoqIDE auto completion doesn't work for some tactics: nothing shows up when typing inside a proof "refl" or "cong".
It used to work for me in previous versions. It does suggest completions for names of earlier lemmas.
Does it behave the same for other CoqIDE users here?
Does anyone know whether this change is intended or should I report an issue?
Which is your current version?
8.12 on macOS 10.15
Last updated: Oct 03 2023 at 19:01 UTC