Stream: Coq users

Topic: CoqIDE auto completion


view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 09 2020 at 11:15):

Which is your current version?

view this post on Zulip Ori Lahav (Nov 09 2020 at 11:52):

8.12 on macOS 10.15


Last updated: Jan 29 2023 at 01:02 UTC