Stream: Coq users

Topic: CoqIDE auto completion

Ori Lahav (Nov 09 2020 at 06:53):

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?
Thanks

Paolo Giarrusso (Nov 09 2020 at 11:15):

Which is your current version?

Ori Lahav (Nov 09 2020 at 11:52):

8.12 on macOS 10.15

Last updated: Oct 03 2023 at 19:01 UTC