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