Suite révision 10495

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

1 files changed, 5 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 17eea233a..d45698d5b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -90,6 +90,11 @@ Tactic Language
   must not be used elsewhere as variables in the same ltac expression
   (possible source of incompatibility).
 - New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
+- "let rec ... in ... " now supports for expressions without explicit
+  parameters; interpretation is lazy to the contrary of "let ... in ...";
+  hence, the "rec" keyword can be used to turn the argument of a
+  "let ... in ..." into a lazy one.
+
 
 Tactics