diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 9 |
1 files changed, 0 insertions, 9 deletions
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: |