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?
> 

In fact it is called with an uppercase.
Try:

✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂

Require Import Utf8.

Example test : ∀ (x:unit),
                 (λ x, x = tt) x.
 now intros [].
Qed.

✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂✂

In fact it seems that Utf8_core is more complete.
I think that this typo should be corrected in the reference manual.