diff options
| author | Théo Zimmermann | 2016-10-18 16:51:21 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2016-10-18 16:51:21 +0200 |
| commit | 6791a37b4e4ba9be829959b419e37a96e2eb5b84 (patch) | |
| tree | fcf1ebc517247fdf45e32be4f4a24e5636a20b71 | |
| parent | 17ec7a0c875014e5322f6098dcd2014072cde9d8 (diff) | |
Document info_auto.
Now that this tactic has been fixed (commit 58d1381),
it needed to get documented.
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 |
1 files changed, 6 insertions, 0 deletions
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 |