The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

Thanks Pierre and Adam. I should have consulted the documentation but I was pressed for time. I think what confused me was the fact that Coq raises a warning if you use "Variable" at global scope, but it doesn't raise a warning if you use "Definition" at local scope. I presume that's because local scope is nested within global scope.

Regards,

Jeff.

On 5 Jun 2013, at 16:36, Pierre Courtieu wrote:

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.