Improving reference manual in that auto uses simple apply rather than apply.

Still, there are small differences, e.g. on
"use_metas_eagerly_in_conv_on_closed_terms", but also maybe in some
amount of use of delta that Matthieu would know better than me if it
matters or not in practice.

1 files changed, 28 insertions, 23 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fa6f783934..06431055ad 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3394,7 +3394,7 @@ local definition. Example: {\tt unfold not in (Type of H1) (Type of H3).}
 This tactic implements a Prolog-like resolution procedure to solve the
 current goal. It first tries to solve the goal using the {\tt
   assumption} tactic, then it reduces the goal to an atomic one using
-{\tt intros} and introducing the newly generated hypotheses as hints.
+{\tt intros} and introduces the newly generated hypotheses as hints.
 Then it looks at the list of tactics associated to the head symbol of
 the goal and tries to apply one of them (starting from the tactics
 with lower cost). This process is recursively applied to the generated
@@ -3454,11 +3454,10 @@ intact. \texttt{auto} and \texttt{trivial} never fail.
 \tacindex{eauto}
 \label{eauto}
 
-This tactic generalizes {\tt auto}. In contrast with
-the latter, {\tt eauto} uses unification of the goal
-against the hints rather than pattern-matching
-(in other words, it uses {\tt eapply} instead of
-{\tt apply}).
+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}).
 As a consequence, {\tt eauto} can solve such a goal:
 
 \begin{coq_eval}
@@ -3623,21 +3622,27 @@ The {\hintdef} is one of the following expressions:
 \item {\tt Resolve \term}
   \comindex{Hint Resolve}
 
-  This command adds {\tt apply {\term}} to the hint list
+  This command adds {\tt simple apply {\term}} to the hint list
   with the head symbol of the type of \term. The cost of that hint is
-  the number of subgoals generated by {\tt apply {\term}}.
-
-  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 be reduced to a type starting with a product, the tactic {\tt
-    apply {\term}} is also stored in the hints list.
-
-  If the inferred type of \term\ contains a dependent
-  quantification on a predicate, it is added to the hint list of {\tt
-    eapply} instead of the hint list of {\tt apply}. In this case, a
-  warning is printed since the hint is only used by the tactic {\tt
-    eauto} (see \ref{eauto}). A typical example of a hint that is used
-  only by \texttt{eauto} is a transitivity lemma.
+  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
+
+  The cost of that hint is the number of subgoals generated by that
+  tactic.
+
+  % 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.
+
+  If the inferred type of \term\ contains a dependent quantification
+  on a variable which occurs only in the premisses of the type and not
+  in its conclusion, no instance could be inferred for the variable by
+  unification with the goal. In this case, the hint is added to the
+  hint list of {\tt eauto} (see \ref{eauto}) instead of the hint list
+  of {\tt auto} and a warning is printed. A typical example of a hint
+  that is used only by \texttt{eauto} is a transitivity lemma.
 
   \begin{ErrMsgs}
   \item \errindex{Bound head variable}
@@ -3649,7 +3654,7 @@ The {\hintdef} is one of the following expressions:
 
     The type of {\term} contains products over variables that do not
     appear in the conclusion. A typical example is a transitivity axiom.
-    In that case the {\tt apply} tactic fails, and thus is useless.
+    In that case the {\tt simple apply} tactic fails, and thus is useless.
 
   \end{ErrMsgs}
 
@@ -3664,10 +3669,10 @@ The {\hintdef} is one of the following expressions:
 \item \texttt{Immediate {\term}}
 \comindex{Hint Immediate}
 
-  This command adds {\tt apply {\term}; trivial} to the hint list
+  This command adds {\tt simple apply {\term}; trivial} to the hint list
   associated with the head symbol of the type of {\ident} in the given
   database. This tactic will fail if all the subgoals generated by
-  {\tt apply {\term}} are not solved immediately by the {\tt trivial}
+  {\tt simple apply {\term}} are not solved immediately by the {\tt trivial}
   tactic (which only tries tactics with cost $0$).
 
   This command is useful for theorems such as the symmetry of equality