The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Tue, 07 Feb 2012 15:30:55 -0800,
Ian Zimmerman 
<itz AT buug.org>
 a écrit :

> 
> Sorry to bother the list with a trivial question.
> 
> The Refman says (section 15.9.1):
> 
>  There exists a small set of such notations already defined, in the
> file utf8.v of Coq library, so you may enable them just by Require
> utf8 inside CoqIDE, or equivalently, by starting CoqIDE with coqide
> -l utf8.
> 
> but my copy of coq doesn't seem to include such a file.
> 
> I'm on debian testing ("Wheezy").  Perhaps the debian maintainer
> dropped it by accident?
> 

And by the way, for the command line, it is more complicate:

"coqide -l theories/Unicode/Utf8"

(and of course Utf8 is also available under ProofGeneral and coqtop).

Note also that you don't really need them to have unicode, unicode is
natively supported by Coq, the only thing is that by default there is
no notation for "forall".

So if you add the line:

Notation "∀ x , t" := (forall x, t) (ident x, at level 80).

you will also have a basic notation (not as fine as the one provided
by Utf8.v, though). For more information, go to the svn repository and
browse the theory files (if you have the sources installed it is even
simpler/better).

https://gforge.inria.fr/scm/viewvc.php/trunk/theories/?root=coq

Oups, check about my last comment in Utf8_core; I think it used to
be the case in 8.3, but in trunk it is not the case anymore, I don't
know if this modification has been backported or if you are using a
newer version.
https://gforge.inria.fr/scm/viewvc.php/trunk/theories/Unicode/Utf8.v?root=coq&r1=13323&r2=14607

By the way, this library has nothing special in regards to any other
one, so if you have a problem with it, it is likely that your
installation is broken, and you may have problems with any other
library as well.