diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-12-07 22:27:19 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-12-11 13:34:55 +0100 |
| commit | 3cc8915e19e3ab85493a459d5e2be221b19592bc (patch) | |
| tree | 96d160bfe23cb63a8ee030c69938ed7e0ab0b196 /plugins/ltac | |
| parent | ac2b757a7835672ba494bf42244b5d393e8db089 (diff) | |
Remove deprecated appcontext and corresponding documentation.
Diffstat (limited to 'plugins/ltac')
| -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 872bea612..ebf6e450b 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: |