aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-01-13 14:28:56 +0000
committerGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-01-13 14:28:56 +0000
commit0224b036502016e9bd4e8b683af458248fdac4a9 (patch)
tree6edb63dd6839906dc95c1c1c5ef29a25e1c67673 /CHANGES
parent204ca2560751eaa0fc00f6d5235fc81236855f1b (diff)
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
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES2
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