From 686f2ecc39bd4dad838476c481f7b38d2cc54205 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 26 Dec 2011 16:48:34 +0000
Subject: update CHANGES w.r.t. simpl

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14863 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 8 ++++++--
 1 file 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
 
-- 
cgit v1.2.3