Merge PR #6169: Clean up/deprecated options

7 files changed, 10 insertions, 22 deletions

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 8b9eb3983..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
@@ -242,12 +237,7 @@ GEXTEND Gram
   match_pattern:
     [ [ IDENT "context";  oid = OPT Constr.ident;
           "["; pc = Constr.lconstr_pattern; "]" ->
-        let mode = not (!Flags.tactic_context_compat) in
-        Subterm (mode, oid, pc)
-      | IDENT "appcontext";  oid = OPT Constr.ident;
-          "["; pc = Constr.lconstr_pattern; "]" ->
-        warn_deprecated_appcontext ~loc:!@loc ();
-        Subterm (true,oid, pc)
+        Subterm (oid, pc)
       | pc = Constr.lconstr_pattern -> Term pc ] ]
   ;
   match_hyps:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6aa2f6f89..e5ff47356 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -526,11 +526,9 @@ let pr_goal_selector ~toplevel s =
 
   let pr_match_pattern pr_pat = function
     | Term a -> pr_pat a
-    | Subterm (b,None,a) ->
-    (** ppedrot: we don't make difference between [appcontext] and [context]
-        anymore, and the interpretation is governed by a flag instead. *)
+    | Subterm (None,a) ->
       keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]"
-    | Subterm (b,Some id,a) ->
+    | Subterm (Some id,a) ->
       keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]"
 
   let pr_match_hyps pr_pat = function
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9bd3efc6b..ccd555b61 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -81,7 +81,7 @@ type 'a with_bindings_arg = clear_flag * 'a with_bindings
 (* Type of patterns *)
 type 'a match_pattern =
   | Term of 'a
-  | Subterm of bool * Id.t option * 'a
+  | Subterm of Id.t option * 'a
 
 (* Type of hypotheses for a Match Context rule *)
 type 'a match_context_hyps =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index b16b0a7ba..ebffde441 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -428,9 +428,9 @@ let intern_hyp_location ist ((occs,id),hl) =
 
 (* Reads a pattern *)
 let intern_pattern ist ?(as_type=false) ltacvars = function
-  | Subterm (b,ido,pc) ->
+  | Subterm (ido,pc) ->
       let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in
-      ido, metas, Subterm (b,ido,pc)
+      ido, metas, Subterm (ido,pc)
   | Term pc ->
       let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
       None, metas, Term pc
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9e47db1c3..32a3b53fd 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1040,7 +1040,7 @@ let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) =
     (bvars,instantiate_pattern env sigma lfun pat)
 
 let read_pattern lfun ist env sigma = function
-  | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
+  | Subterm (ido,c) -> Subterm (ido,eval_pattern lfun ist env sigma c)
   | Term c -> Term (eval_pattern lfun ist env sigma c)
 
 (* Reads the hypotheses of a Match Context rule *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 918d1faeb..79bf3685e 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -121,7 +121,7 @@ let subst_raw_may_eval subst = function
   | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c)
 
 let subst_match_pattern subst = function
-  | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc))
+  | Subterm (ido,pc) -> Subterm (ido,(subst_glob_constr_or_pattern subst pc))
   | Term pc -> Term (subst_glob_constr_or_pattern subst pc)
 
 let rec subst_match_goal_hyps subst = function
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 89b78e590..e87951dd7 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -237,7 +237,7 @@ module PatternMatching (E:StaticEnvironment) = struct
             return lhs
           with Constr_matching.PatternMatchingFailure -> fail
         end
-    | Subterm (with_app_context,id_ctxt,p) ->
+    | Subterm (id_ctxt,p) ->
 
       let rec map s (e, info) =
         { stream = fun k ctx -> match IStream.peek s with
@@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct
             | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
         }
       in
-      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
+      map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error
 
 
   (** [rule_match_term term rule] matches the term [term] with the