Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Unicode tokens?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unicode tokens?


Chronological Thread 
  • From: Tom Hirschowitz <tom.hirschowitz AT univ-smb.fr>
  • To: "Paul A. Steckler" <steck AT stecksoft.com>, coq-club <coq-club AT inria.fr>
  • Cc:
  • Subject: Re: [Coq-Club] Unicode tokens?
  • Date: Tue, 07 Mar 2017 21:02:22 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tom.hirschowitz AT univ-smb.fr; spf=SoftFail smtp.mailfrom=tom.hirschowitz AT univ-smb.fr; spf=None smtp.helo=postmaster AT smtpout01.partage.renater.fr

Aha, right, I've already encountered this one, but had forgotten.

Apparently, company-coq isn't much better: it displays something like
delta₁.

Good luck!
Tom

"Paul A. Steckler"
<steck AT stecksoft.com>
writes:

> On Tue, Mar 7, 2017 at 5:43 AM, Tom Hirschowitz
> <tom.hirschowitz AT univ-smb.fr>
> wrote:
>> What kind of bugs are you thinking of?
>
> For example, in the PG file coq/example-tokens.v, there is the text
> "delta__1", which should show a subscripted Greek letter. Instead, the
> text appears verbatim.
>
> I think I've tracked down this bug to the regular expression that's
> generated for token matching.
>
> -- Paul

Archive powered by MHonArc 2.6.18.

Top of Page