New cleaning phase of the Local/Global option management

- Clarification and documentation of the different styles of
  Local/Global modifiers in vernacexpr.ml
- Addition of Global in sections for Open/Close Scope.
- Addition of Local for Ltac when not in sections.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 563ab83ad..681bd791d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -56,6 +56,8 @@ Vernacular commands
   referring to the constant by a notation string.
 - Added "Reserved Infix" as a specific shortcut of the corresponding
   "Reserved Notation".
+- Open/Close Scope command supports Global option in sections.
+- Ltac definitions support Local option for non-export outside modules.
 
 Tools