coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Coq and Unicode

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Coq and Unicode
Date: Sat, 3 Aug 2019 07:45:35 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga14.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.600.7
Ironport-phdr: 9a23:vSoVxhJqngr5UVqxYdmcpTZWNBhigK39O0sv0rFitYgfKPzxwZ3uMQTl6Ol3ixeRBMOHsqgC0rKO+Pm6AiQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagf79+Ngi6oRnNusUZnIduNKg8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMDE37XzXitdojK1FvB2huxJxw4nRYI6PNfp+eL7WcdcVSGdFW8pcUTFKDIGhYIsVF+cPPfhWoZThp1UArhW+CwujBOLzxTBHiXH7xrE63P8lHA3awAAsA9ADvXLJp9v1LqcSVuW1wbHGwTveaPNZxzj96JTSchAmufGARa97f83QyUYzFwPKlEufqYjrMziI0ekNtmmb4PZgVe21lWEnrxt9oiOoxsgyhYnJmpgVylfc9ShiwYY1I8G4R1B/YdK+DJRQsCSaOpJwT8g/TW9ovyM6xacHuZ69ZCUKx5UnxwLfa/yaaIeE+BPjVOGJLTd5gnJlZKywhxKo/Ue91OLxUNS/3lVSriddj9XBsm4B2wbT58WHUPdw/lmt1SyS2wzO6uxIOV04mKvVJpI7zLM9mIAfvVrNEyLygkn6kaybels89uS16unqZq/qqoGcOoJ7kA3yLL4il8y7DOk+LwMARXKU+f6m273m5UD5QKtFjvkxkqTBtZDaKt4UqrO2DgNP04Yj7Qq/ACmi0NgCgXYHK1dFdAqGj4jvJV7OPOj1Aeq7jliyijtmx/DLMqfhD5nTNHTPjartcLZl505Z0gUzzNRf55xOCrEGJfL+QkrxtN3EAR85KQO73eLnBM9m1oMZR22PDbOZMLnVsV+Q/e8vIu+MZJMLtzb5MfQq+/nujXohlV8HYaapxYcXaGy/Hvl+P0qZZmPsjs4dHmcOowoxV/fniEaCUD5Wf3a9Rbgw5jA9CIK8DIfMXJqhgLKb3HTzIpoDLGtBExWHFWriX4SCQfYFLiyIaIc1mTsdELOlVoUJ1Be0tQa8xaAxfcTO/ShN/6nk2ddp/erL0VkX9Dd0BsmZmSnZSmB/nmoFQ3kt261wvVZ60n+C17R1h7pTEtkFtKABaRszKZOJl78yMNv1QA+UIobQFQSWB+6+CDR0deofht8DZ0EkRIengRmag2yrBaMYk/qAA5lmqvuAjUi0HN50zjP97Idkl0MvG5IdNGu6i6o5/A/WVdaQwhep0p2yfKFZ5xbjsWKKzG6ApkZdCVciUKPZUHRZbUzT/430

Hi Theo,

> The situation has become better in CoqIDE "out of the box" in version
> 8.10 thanks to the effort by Arthur Charguéraud. See the documentation
> here: https://coq.github.io/doc/V8.10+beta2/refman/practical-
> tools/coqide.html#coqide-unicode

I just tested in on Windows on a fairly recent 8.10 build and Shift+Space
simply inserts a space here. Can you confirm that it works on Linux on 8.10?

The chosen font would support Unicode.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

Re: [Coq-Club] Coq and Unicode, Benjamin C. Pierce, 08/02/2019
- <Possible follow-up(s)>
- RE: [Coq-Club] Coq and Unicode, Soegtrop, Michael, 08/03/2019
  - Re: [Coq-Club] Coq and Unicode, Théo Zimmermann, 08/03/2019