From 9ba579bb98ac8e8964a9baea376ce0c9a89f2615 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 09:59:32 +0100
Subject: CHANGES: Info command + info_auto currently broken.

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

diff --git a/CHANGES b/CHANGES
index 19da2a4c81..712a8a7e92 100644
--- a/CHANGES
+++ b/CHANGES
@@ -260,6 +260,12 @@ Tactics
     an inductive type with indices is fixed
   - residual local definitions are now correctly removed.
 - The rename tactic may now replace variables in parallel.
+- A new "Info" command replaces the "info" tactical discontinued in
+  v8.4. It still gives informative results in many cases.
+- The "info_auto" tactic is known to be broken and does not print a
+  trace anymore. Use "Info 1 auto" instead. The same goes for
+  "info_trivial". On the other hand "info_eauto" still works fine,
+  while "Info 1 eauto" prints a trivial trace.
 
 Program
 
-- 
cgit v1.2.3