update CHANGES w.r.t. simpl

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

1 files changed, 6 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 83e34ddfc0..5bcdae6e4a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -69,6 +69,11 @@ Tactics
   used now instead of enumerating all remaining constructors. Moreover, the
   pattern "match _ with _ => _ end" now allows to match any "match". A "in"
   annotation can also be added to restrict to a precise inductive type.
+- The behavior of "simpl" can be tuned using the "Arguments" vernacular.
+  In particular constants can be marked so that they are always/never unfolded
+  by "simpl", or unfolded only when a set of arguments evaluates to a
+  constructor. Last one can mark a constant so that it is unfolded only if the
+  simplified term does not expose a match in head position.
 
 Vernacular commands
 
@@ -95,8 +100,7 @@ Vernacular commands
   over a given list of section variables at section ending (DOC TODO).
 - New command "Arguments" generalizing "Implicit Arguments" and
   "Arguments Scope" and that also allows to rename the parameters of a
-  definition and to force some arguments of a definition to be
-  constructors before tactic "simpl" accepts to unfold this definition.
+  definition and to tune the behavior of the tactic "simpl".
 
 Module System