Fix description of change in intro semantics.

1 files changed, 4 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index f7e1dee4c..c3eaae6ee 100644
--- a/CHANGES
+++ b/CHANGES
@@ -50,9 +50,10 @@ Tactics
 - Every generic argument type declares a tactic scope of the form "name:(...)"
   where name is the name of the argument. This generalizes the constr: and ltac:
   instances.
-- When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use
-  a locally free identifier anymore. It must use e.g. the "fresh" primitive
-  instead (potential source of incompatibilities).
+- When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is
+  given a free identifier, it is not bound in subsequent tactics anymore.
+  In order to introduce a binding, use e.g. the "fresh" primitive instead
+  (potential source of incompatibilities).
 - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO).
 - New goal selectors.  Sets of goals can be selected by select by listing
   integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24.