Module names and constant/inductive names are now in two separate namespaces

 We now accept the following code: Definition E := 0. Module E. End E.

 Techically, we simply allow the same label to occur at most twice in
 a structure_body, which is a (label * structure_field_body) list).
 These two label occurences should not be at the same level of fields
 (e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or
 a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change.
 Drawback : no more simple List.assoc or equivalent should be performed
 on a structure_body ...

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

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index b38a346a04..cdcda4ed11 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,12 @@ Program
   consistent with "Proof with".
 - Program Lemma, Definition now respect automatic introduction.
 
+Module System
+
+- The names of modules (and module types) are now in a fully separated
+  namespace from ordinary definitions : "Definition E:=0. Module E. End E."
+  is now accepted.
+
 CoqIDE
 
 - Coqide now supports the Restart command, and Undo (with a warning).