Making the behavior of "injection ... as ..." more natural:

- hypotheses are introduced in the left-to-right order
- intropatterns have to match the number of generated hypotheses, and,
  if less, new introduction names are automatically generated
- clearing the hypothesis on which injection is applied, if any.

However, this is a source of incompatibilities (for a variant of
injection that is hopefully not used a lot). Compatibility can be
restored by "Unset Injection L2R Pattern Order".

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

1 files changed, 6 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index 6e0e434782..eb39ac34e0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -50,7 +50,12 @@ Tactics
   "context" can be retrieved at parse time by setting the
   "Tactic Compat Context" flag. (possible source of incompatibilities).
 - Introduction patterns of the form [x1 .. xn] or (x1,..,xn) now apply
-  injection when used on an equality statement ("ssreflect" style)
+  "injection" when used on an equality statement ("ssreflect" style).
+- Tactic "injection c as ipats" now clears c if c refers to an
+  hypothesis and moves the resulting equations in the hypotheses
+  independently of the number of ipats, which has itself to be less
+  than the number of new hypotheses (possible source of incompatibilities;
+  former behavior obtainable by "Unset Injection L2R Pattern Order").
 
 Program