Incorrect use of Unicode symbol in error message for Coq

ProofGeneral / PG

This repo is the new home of Proof General

https://proofgeneral.github.io

GNU General Public License v3.0

492 stars 88 forks source link

Incorrect use of Unicode symbol in error message for Coq #616

Open fblanqui opened 3 years ago

fblanqui commented 3 years ago

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 commented 3 years ago

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.