Construct "T with (Definition|Module) id := c" generalized to

"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style).


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

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 098ab23ff..9610e84f8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,6 +35,8 @@ Modules
 - Added syntactic sugar "Module M(Export/Import X Y: T)" and
   "Module Type M(Export/Import X Y: T)"
   (only for interactive definitions) (doc TODO)
+- Construct "with" generalized to module paths:
+   T with (Definition|Module) M1.M2....Mn.l := l'.  (doc TODO)
 
 Notations