Revising r16550 about providing intro patterns for applying injection:

- Introduction of a specific notation for injection intropatterns: [= pats]
- Use of this specific pattern also to apply discriminate on the fly

Note: The automatic injection of dependent tuples over a same first
component (introduced in r10180) still not integrated to the main
parts of injection and its variant (indeed, it applies only for a root
dependent tuple in sigT).

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

1 files changed, 4 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 8cea62915..0cb2b7bdf 100644
--- a/CHANGES
+++ b/CHANGES
@@ -49,8 +49,10 @@ Tactics
 - Now "appcontext" and "context" behave the same. The old buggy behaviour of
   "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).
+- New introduction pattern [= x1 .. xn] applies "injection as [x1 .. xn]"
+  on the fly if next hypothesis to introduce is an injectible equality
+  (idea borrowed from Georges Gonthier). Introduction pattern [=] applies
+  "discriminate" if a discriminable equality.
 - 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