aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index a7dec737a7..f06cbb2e10 100644
--- a/CHANGES
+++ b/CHANGES
@@ -94,6 +94,8 @@ Vernacular commands
- Include Type is now deprecated since Include now accept both modules and
module types.
- Declare ML Module supports Local option.
+- New command "Declare Reduction <id> := <conv_expr>", allowing to write
+ later "Eval <id> in ...". This command accepts a Local variant.
Tools