2 files changed, 27 insertions, 12 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 587f4e5cb3..9378529cbe 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1289,7 +1289,7 @@ Prints a profile for all tactics that start with {\qstring}. Append a period (.)
 \begin{quote}
 {\tt Reset Ltac Profile}.
 \end{quote}
-Resets the profile, that is, deletes all accumulated information
+Resets the profile, that is, deletes all accumulated information.  Note that backtracking across a {\tt Reset Ltac Profile} will not restore the information.
 
 \begin{coq_eval}
 Reset Initial.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index c5fd40bf15..2da12c8d69 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2289,6 +2289,12 @@ giving \texttt{injection {\term} as} (with an empty list of names). To
 obtain this behavior, the option {\tt Set Structural Injection} must
 be activated. This option is off by default.
 
+By default, \texttt{injection} only creates new equalities between
+terms whose type is in sort \texttt{Type} or \texttt{Set}, thus
+implementing a special behavior for objects that are proofs
+of a statement in \texttt{Prop}.  This behavior can be turned off
+by setting the option \texttt{Set Keep Proof Equalities}.
+\optindex{Keep Proof Equalities}
 \subsection{\tt inversion \ident}
 \tacindex{inversion}
 
@@ -2308,6 +2314,14 @@ latter is first introduced in the local context using
 stock the lemmas whenever the same instance needs to be inverted
 several times. See Section~\ref{Derive-Inversion}.
 
+\Rem Part of the behavior of the \texttt{inversion} tactic is to generate
+equalities between expressions that appeared in the hypothesis that is
+being processed.  By default, no equalities are generated if they relate
+two proofs (i.e. equalities between terms whose type is in
+sort \texttt{Prop}).  This behavior can be turned off by using the option
+\texttt{Set Keep Proof Equalities.}
+\optindex{Keep Proof Equalities}
+
 \begin{Variants}
 \item \texttt{inversion \num}
 
@@ -4356,22 +4370,23 @@ vernacular command and printed using {\nobreak {\tt Print Firstorder
 
    Tries to solve the goal with {\tac} when no logical rule may apply.
 
- \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
-   \tacindex{firstorder with}
-
-   Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search
-   environment.
-
  \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ }
    \tacindex{firstorder using}
 
-   Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$
-   to the proof-search environment. If {\qualid}$_i$ refers to an inductive
-   type, it is the collection of its constructors which is added as hints.
+   Adds lemmas {\qualid}$_1$ \dots\ {\qualid}$_n$ to the proof-search
+   environment. If {\qualid}$_i$ refers to an inductive type, it is
+   the collection of its constructors which are added to the
+   proof-search environment.
 
-\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+ \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
+   \tacindex{firstorder with}
 
-  This combines the effects of the {\tt using} and {\tt with} options.
+   Adds lemmas from {\tt auto} hint bases \ident$_1$ \dots\ \ident$_n$
+   to the proof-search environment.
+
+\item \texttt{firstorder {\tac} using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+
+  This combines the effects of the different variants of \texttt{firstorder}.
 
 \end{Variants}