Announcing * and ** which were not official yet in 8.4.

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 53cec0061f..982b96a115 100644
--- a/CHANGES
+++ b/CHANGES
@@ -216,6 +216,8 @@ Tactics
   on the fly if injection is applicable to the hypothesis under consideration
   (idea borrowed from Georges Gonthier). Introduction pattern [=] applies
   "discriminate" if a discriminable equality.
+- New introduction patterns * and ** to respectively introduce all forthcoming
+  dependent variables and all variables/hypotheses dependent or not.
 - 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