Incorrect use of Unicode symbol in error message for Coq

[fblanqui]

With the following code:

Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Scheme paths_ind := Induction for paths Sort Type.

I get the following error message:

Error: paths_ind already ∃.

When I do copy and paste, ∃ is replaced by "exists". Not sure it is related to PG though as I use company-coq as well.

[Matafou]

Hi @fblanqui. This is a known bug of both company-coq (with prettify-symbol enabled) and pg (unicode-tokens). I am afraid we can't fix this until PG is based on a good protocol with distinction between raw text and terms.

ping @cpitclaudel.