The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT loria.fr>]

Dear all,

With Coq-8.0beta, I was used to be able to define abreviations in an
environment where all subterms they refered to where not defined.

For instance, I could define :

Notation Symbol := (symbol Sig).

whereas Sig was not defined.

This worked, because each time the Symbol notation was used, Sig was
indeed present in the environment.

But now, it seems that with Coq-8.0 Sig is required to be defined be fore the
Notation command, which is a big problem for me.

Has someone information on this topic ?

Many thanks in advance,
Sébastien.