From 6791a37b4e4ba9be829959b419e37a96e2eb5b84 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 18 Oct 2016 16:51:21 +0200
Subject: Document info_auto.

Now that this tactic has been fixed (commit 58d1381),
it needed to get documented.
---
 doc/refman/RefMan-tac.tex | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fc6d9c143c..dccd6f5907 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3490,6 +3490,12 @@ hints of the database named {\tt core}.
 
   This combines the effects of the {\tt using} and {\tt with} options.
 
+\item {\tt info\_auto}
+
+  Behaves like {\tt auto} but shows the tactics it uses to solve the goal.
+  This variant is very useful for getting a better understanding of automation,
+  or to know what lemmas/assumptions were used.
+
 \item {\tt trivial}\tacindex{trivial}
 
   This tactic is a restriction of {\tt auto} that is not recursive and
-- 
cgit v1.2.3