Fix bug #4923: Warning: appcontext is deprecated.

9 files changed, 18 insertions, 18 deletions

diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v
index a19e9df90..7e3ef8929 100644
--- a/plugins/micromega/Env.v
+++ b/plugins/micromega/Env.v
@@ -93,7 +93,7 @@ End S.
 Ltac jump_simpl :=
   repeat
     match goal with
-      | |- appcontext [jump xH] => rewrite (jump_simpl xH)
-      | |- appcontext [jump (xO ?p)] => rewrite (jump_simpl (xO p))
-      | |- appcontext [jump (xI ?p)] => rewrite (jump_simpl (xI p))
+      | |- context [jump xH] => rewrite (jump_simpl xH)
+      | |- context [jump (xO ?p)] => rewrite (jump_simpl (xO p))
+      | |- context [jump (xI ?p)] => rewrite (jump_simpl (xI p))
     end.
diff --git a/test-suite/bugs/closed/2839.v b/test-suite/bugs/closed/2839.v
index e396fe06e..e727e2606 100644
--- a/test-suite/bugs/closed/2839.v
+++ b/test-suite/bugs/closed/2839.v
@@ -5,6 +5,6 @@ intro.
 Fail
   let H :=
     match goal with
-    | [ H : appcontext G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H'
+    | [ H : context G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H'
     end
   in pose H.
diff --git a/test-suite/bugs/closed/3563.v b/test-suite/bugs/closed/3563.v
index 679721667..961563ed4 100644
--- a/test-suite/bugs/closed/3563.v
+++ b/test-suite/bugs/closed/3563.v
@@ -16,11 +16,11 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> H * H0)
        transport (fun y : H1 -> H * H0 => H5 (fst (y H2))) H4 H6 = H7.
   intros.
   match goal with
-    | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ]
+    | [ |- context ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ]
       => set(foo:=h); idtac
   end.
   match goal with
-    | [ |- appcontext ctx [transport (fun y => (?g (fst (y H2))))] ]
+    | [ |- context ctx [transport (fun y => (?g (fst (y H2))))] ]
       => idtac
   end.
 Abort.
@@ -30,7 +30,7 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> (H1 -> H) * H0)
        transport (fun y : H1 -> (H1 -> H) * H0 => H5 (fst (y H2) H2)) H4 H6 = H7.
   intros.
   match goal with
-    | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ]
+    | [ |- context ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ]
       => set(foo:=X)
   end.
 (* Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index f85a60264..eb37141bc 100644
--- a/test-suite/bugs/closed/4198.v
+++ b/test-suite/bugs/closed/4198.v
@@ -11,7 +11,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
   simpl.
   intros.
   match goal with
-    | [ |- appcontext G[@hd] ] => idtac
+    | [ |- context G[@hd] ] => idtac
   end.
 
 (* This second example comes from CFGV where inspecting subterms of a
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index 008fb72c4..73da464bb 100644
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -22,8 +22,8 @@ Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := o
 
 Ltac present_obj from to :=
   match goal with
-           | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in *
-           | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
+           | [ _ : context[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in *
+           | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
          end.
 
 Section NaturalTransformationComposition.
diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v
index 5e5d5ab3e..3d16e7ac0 100644
--- a/test-suite/bugs/closed/HoTT_coq_058.v
+++ b/test-suite/bugs/closed/HoTT_coq_058.v
@@ -95,10 +95,10 @@ Goal forall (T : Type) (T0 : T -> T -> Type)
                            | tt => idpath
                          end)) (x1; p) = (x1; p).
 intros.
-let F := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in
-let H := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in
-let X := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in
-let T := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in
+let F := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in
+let H := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in
+let X := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in
+let T := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in
 let t0 := fresh "t0" in
 let t1 := fresh "t1" in
 let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in
@@ -116,7 +116,7 @@ let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in
               let GL1' := fresh in
               set (GL0' := GL0);
 
-                let arg := match GL0 with appcontext[x0 ?arg] => constr:(arg) end in
+                let arg := match GL0 with context[x0 ?arg] => constr:(arg) end in
                 assert (t1 = arg) by (subst t1; reflexivity); subst t1;
                 pattern (x0 arg) in GL0';
                 match goal with
diff --git a/test-suite/bugs/opened/3383.v b/test-suite/bugs/opened/3383.v
index 9a14641a5..c04b6b7b4 100644
--- a/test-suite/bugs/opened/3383.v
+++ b/test-suite/bugs/opened/3383.v
@@ -1,7 +1,7 @@
 Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end.
 intro.
 Fail lazymatch goal with
-| [ |- appcontext[match ?b as b' return @?P b' with true => ?t | false => ?f end] ]
+| [ |- context[match ?b as b' return @?P b' with true => ?t | false => ?f end] ]
   => change (match b as b' return P b with true => t | false => f end) with (@bool_rect P t f)
 end. (* Toplevel input, characters 153-154:
 Error: The reference P was not found in the current environment. *)
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 7384790da..dfd6b0eae 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -264,7 +264,7 @@ Ltac bang :=
   match goal with
     | |- ?x =>
       match x with
-        | appcontext [False_rect _ ?p] => elim p
+        | context [False_rect _ ?p] => elim p
       end
   end.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index a2fd05cd9..c490ea516 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -211,7 +211,7 @@ Ltac fold_sub f :=
   match goal with
     | [ |- ?T ] =>
       match T with
-        appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] =>
+        context C [ @Fix_sub _ _ _ _ _ ?arg ] =>
         let app := context C [ f arg ] in
           change app
       end