The Coq mailing list

[Jelle Herold <jelle AT defekt.nl>]

On 02/08/2012 10:16 AM, AUGER Cédric wrote:
> > 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.

They are basically the same file and have been merged, see bug 2610 
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2610

This is fixed in rev 14605, so also in 8.4

Jelle.