Auto-complete suggests commands in proof mode: pretty useless.

[Zimmi48]

Every time I type a space at the beginning of a new sentence (in my case it happens when indenting, i.e. at the beginning of a proof, or of a new bullet), I get auto-complete suggestions of some common Coq commands as shown in the screenshot. In proof mode, this is pretty useless and I would prefer to not see any suggestion at all, or a list of the most commonly used tactics (intros, apply, easy, induction and possibly their SSReflect counter-part if the SSReflect plugin is loaded).

PS: given how bad practice it is, I wish that Global Unset was not in the list of these common commands that are suggested when I type a space.

[maximedenes]

This behavior is new, not sure what changed it. Will investigate.

[TheoWinterhalter]

I think I had it before the update.

[maximedenes]

It seems there are two kinds of snippets provided by VsCoq: some are contributed via the standard extension point, some others are directly registered through the Snippets API. I believe we should migrate everything to the first kind.

[rtetley]

This seems obsolete