The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 2 mars 10 à 09:59, Vladimir Voevodsky a écrit :

> Suppose I have some local definitions in a section which are  
> introduced with [Let].  Then they start showing up in the local  
> environments of all the proofs in the section. How can I ask Coq not  
> to display some of these definitions on the "goals" pages of the  
> proofs?

Dear Vladimir,

  you can use either [Definition]s or [Notation]s instead of [Let]
to define abbreviations that won't appear in the proof context.

Hope this helps,
-- Matthieu