From c01d2f47a8202e7023250e4cfbbebdac6abb3abb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Mar 2015 22:03:01 +0100
Subject: Announcing * and ** which were not official yet in 8.4.

---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

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
-- 
cgit v1.2.3