Syntax highlighting adds an odd box around lower-case unicode letters

[RalfJung]

I often use unicode letters in my Coq identifers, to better match what we do on paper. This works fine in Coq, but the syntax highlighting of this extension draws a box around some these characters:

This makes them look like some sort of error, and also makes them hard to read.

In a plain text file these letters look just right, so it seems to be something specific to what VsCoq does in .v files. This seems to be font-independent; I tried two different monospace fonts and they both show this effect.

[4ever2]

I don't think this is anything specific to VsCoq, it seems to be because of the editor.unicodeHighlight.ambiguousCharacters setting. When enabled it will highlight any ambiguous unicode characters in all non plaintext/markdown files.

[RalfJung]

Thanks for pointing that out! That helps indeed. :) I have no clue why vscode thinks σ could be confused with another charcacter (but, say, Λ could not)... but now I can at least disabled this behavior.