diff options
| author | Théo Zimmermann | 2017-12-07 22:27:19 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-12-11 13:34:55 +0100 |
| commit | 3cc8915e19e3ab85493a459d5e2be221b19592bc (patch) | |
| tree | 96d160bfe23cb63a8ee030c69938ed7e0ab0b196 | |
| parent | ac2b757a7835672ba494bf42244b5d393e8db089 (diff) | |
Remove deprecated appcontext and corresponding documentation.
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 17 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 9 |
2 files changed, 0 insertions, 26 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 7034c56081..8d82460a72 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} diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 872bea612a..ebf6e450b1 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -78,11 +78,6 @@ let test_bracket_ident = let hint = G_proofs.hint -let warn_deprecated_appcontext = - CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated" - (fun () -> strbrk "appcontext is deprecated and will be removed " ++ - strbrk "in a future version") - GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint tactic_mode constr_may_eval constr_eval toplevel_selector @@ -243,10 +238,6 @@ GEXTEND Gram [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> Subterm (oid, pc) - | IDENT "appcontext"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - warn_deprecated_appcontext ~loc:!@loc (); - Subterm (oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: |