The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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?

Thanks!
Vladimir.