The tactic remember now accepts a final eqn:H option (grant wish #2489)

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

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 91e5a33b0..731083273 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,8 @@ Tactics
 - An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
   or "induction" to make it generate equations in the spirit of "case_eq".
   The former syntax "_eqn" is discontinued.
+- The name of the hypothesis introduced by tactic "remember" can be
+  set via the new syntax "remember t as x eqn:H" (wish #2489).
 
 Program