The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

To be more explicit than Adam, if you want to "hide" things (that is: put them in their own namespace) you might want to consider modules instead of sections.

Best,
Pierre

2013/6/4 Adam Chlipala <adamc AT csail.mit.edu>

On 06/04/2013 03:28 AM, Terrell, Jeffrey wrote:

I was surprised to find that y is still in scope after the section is closed.

Definition x : nat := 1.
Print All.
Section P.
    Definition y : nat := 2.
    Print All.
End P.
Print All.

Do definitions (as opposed to declarations) always have global scope? If so, why?
   

Making definitions with global scope (or at least outside-the-section scope) is precisely the purpose of Coq sections.  Perhaps it's worth having look at the manual or another introduction to sections.