Merge remote-tracking branch 'github/pr/326' into v8.5

Was PR#326: Extend documentation of auto

1 files changed, 49 insertions, 12 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 5eb8cedd95..11de4f35e0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3472,7 +3472,7 @@ hints of the database named {\tt core}.
   Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to
   the database {\tt core}. See Section~\ref{Hints-databases} for the
   list of pre-defined databases and the way to create or extend a
-  database.  This option can be combined with the previous one.
+  database.
 
 \item {\tt auto with *}
 
@@ -3486,9 +3486,17 @@ hints of the database named {\tt core}.
   $lemma_i$ is an inductive type, it is the collection of its
   constructors which is added as hints.
 
-\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$
+\item {\tt info\_auto}
 
-  This combines the effects of the {\tt using} and {\tt with} options.
+  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 \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$
+  {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+  \ident$_1$ {\ldots} \ident$_n$}
+
+  This is the most general form, combining the various options.
 
 \item {\tt trivial}\tacindex{trivial}
 
@@ -3500,6 +3508,14 @@ hints of the database named {\tt core}.
 
 \item \texttt{trivial with *}
 
+\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$
+
+\item {\tt info\_trivial}
+
+\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$
+  {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+  \ident$_1$ {\ldots} \ident$_n$}
+
 \end{Variants}
 
 \Rem {\tt auto} either solves completely the goal or else leaves it
@@ -3513,8 +3529,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail.
 
 This tactic generalizes {\tt auto}. While {\tt auto} does not try
 resolution hints which would leave existential variables in the goal,
-{\tt eauto} does try them (informally speaking, it uses {\tt eapply}
-where {\tt auto} uses {\tt apply}).
+{\tt eauto} does try them (informally speaking, it uses
+{\tt simple eapply} where {\tt auto} uses {\tt simple apply}).
 As a consequence, {\tt eauto} can solve such a goal:
 
 \begin{coq_eval}
@@ -3529,8 +3545,17 @@ eauto.
 Abort.
 \end{coq_eval}
 
-Note that {\tt ex\_intro} should be declared as an
-hint.
+Note that {\tt ex\_intro} should be declared as a hint.
+
+\begin{Variants}
+
+\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$
+  {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+  \ident$_1$ {\ldots} \ident$_n$}
+
+  The various options for eauto are the same as for auto.
+
+\end{Variants}
 
 \SeeAlso Section~\ref{Hints-databases}
 
@@ -3684,11 +3709,12 @@ The {\hintdef} is one of the following expressions:
   the number of subgoals generated by {\tt simple apply {\term}}.
 %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
 
-  % Is it really needed?
-  %% In case the inferred type of \term\ does not start with a product
-  %% the tactic added in the hint list is {\tt exact {\term}}. In case
-  %% this type can however be reduced to a type starting with a product,
-  %% the tactic {\tt apply {\term}} is also stored in the hints list.
+  In case the inferred type of \term\ does not start with a product
+  the tactic added in the hint list is {\tt exact {\term}}.
+% Actually, a slightly restricted version is used (no conversion on the head symbol)
+  In case
+  this type can however be reduced to a type starting with a product,
+  the tactic {\tt simple apply {\term}} is also stored in the hints list.
 
   If the inferred type of \term\ contains a dependent quantification
   on a variable which occurs only in the premisses of the type and not
@@ -3718,6 +3744,17 @@ The {\hintdef} is one of the following expressions:
 
     Adds each \texttt{Resolve} {\term$_i$}.
 
+  \item {\tt Resolve -> \term}
+
+    Adds the left-to-right implication of an equivalence as a hint
+    (informally the hint will be used as {\tt apply <- \term},
+    although as mentionned before, the tactic actually used is
+    a restricted version of apply).
+
+  \item {\tt Resolve <- \term}
+
+    Adds the right-to-left implication of an equivalence as a hint.
+
   \end{Variants}
 
 \item \texttt{Immediate {\term}}