From 3cc8915e19e3ab85493a459d5e2be221b19592bc Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 7 Dec 2017 22:27:19 +0100
Subject: Remove deprecated appcontext and corresponding documentation.

---
 plugins/ltac/g_ltac.ml4 | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'plugins')

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:
-- 
cgit v1.2.3