1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index cda16d380..e80a3b454 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,9 @@ Tactics
   incompatibilities as soon as the inductive types have dependencies in
   the type of their constructors; "double induction" remains however
   deprecated).
+- In introduction patterns of the form (pat1,...,patn), n should match
+  the exact number of hypotheses introduced (except for local definitions
+  for which pattern can be omitted, as in regular pattern-matching).
 
 Program