The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

Hello,
it seems that Proofgeneral has some problems with coq 8.3 in presence of 
unicode symbols. For me, the response buffer fails to correctly show type 
errors when the input phrase contains unicode symbols. Try for instance: 
Check 0 ≠ true. 
Check let α := true in α + 5. 
Check λ x => 0. 
Instead of highlighting the expression that raises the type error in the main 
buffer, the response buffer reprints the input phrase followed by some non-
printing control characters and then shows the usual error message (see 
attached file).
Can anybody confirm this problem?
Is this a bug in coqtop or was something changed on purpose and Proofgeneral 
has to be adapted?
-- 
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France
Toplevel input, characters 28-29:
> Check λ x => x.
>         ^
Error: Cannot infer the type of x.