The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

It looks like input encoding actually refers to "output encoding", perhaps because it is from the viewpoint of the system (latex/browser) that reads coqdoc output.

If so, -utf8 specifies a more expressive output character set where such fancy math symbols are available.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, Aug 26, 2014 at 4:06 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

That worked. Thanks. But is this a bug? Documentation says -utf8 is for setting input file encoding. How is this related with using pretty-printed symbols in output file?

---
Ömer Sinan Ağacan
http://osa1.net

2014-08-26 22:38 GMT+03:00 Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

try:

coqdoc -utf8 MyFile.v

On my system,  -> is printed iff I use the -utf8  flag.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, Aug 26, 2014 at 3:34 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

That didn't work and I think it'd be really weird if it worked.

---
Ömer Sinan Ağacan
http://osa1.net

2014-08-26 22:19 GMT+03:00 Roger Witte <rogerwite AT yahoo.co.uk>:

Try Require Import Utf 8.

Sent from Yahoo Mail on Android

---

From: Ömer Sinan Ağacan <omeragacan AT gmail.com>;
To: coq club <coq-club AT inria.fr>;
Subject: [Coq-Club] coqdoc doesn't pretty-print
Sent: Tue, Aug 26, 2014 7:16:59 PM

As far as I can understand from reference manual, Coq should
pretty-print some symbols like ->, |-, \/ etc. by default but `coqdoc
MyFile.v` generates a HTML with non-pretty-printed symbols. Any ideas
what I'm missing? I don't have any `printing` directives in the source
file, it's just a a dummy file with some random definitions for
testing.

Thanks.

---
Ömer Sinan Ağacan
http://osa1.net