Merge PR #6169: Clean up/deprecated options

1 files changed, 0 insertions, 17 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 7034c5608..8d82460a7 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -198,8 +198,6 @@ is understood as
            {\cpattern} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]}
            {\tt =>} {\tacexpr}\\
-& $|$ & {\tt appcontext} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]}
-           {\tt =>} {\tacexpr}\\
 & $|$ & {\tt \_ =>} {\tacexpr}\\
 \\
 {\it test} & ::= &
@@ -876,21 +874,6 @@ Goal True.
 f (3+4).
 \end{coq_example}
 
-\item \index{appcontext@\texttt{appcontext}!in pattern}
-  \optindex{Tactic Compat Context}
-For historical reasons, {\tt context} used to consider $n$-ary applications
-such as {\tt (f 1 2)} as a whole, and not as a sequence of unary
-applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} would fail
-to find a matching subterm in {\tt (f 1 2)}: if the pattern was a partial
-application, the matched subterms would have necessarily been
-applications with exactly the same number of arguments.
-As a workaround, one could use the following variant of {\tt context}:
-\begin{quote}
-{\tt appcontext} {\ident} {\tt [} {\cpattern} {\tt ]}
-\end{quote}
-This syntax is now deprecated, as {\tt context} behaves as intended. The former
-behavior can be retrieved with the {\tt Tactic Compat Context} flag.
-
 \end{Variants}
 
 \subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal}