s/appcontext/context/

They mean the same thing since 8.5, and appcontext is deprecated.

14 files changed, 40 insertions, 40 deletions

diff --git a/Makefile b/Makefile
index 3324ec86a..1d4020efb 100644
--- a/Makefile
+++ b/Makefile
@@ -76,9 +76,9 @@ COQPRIME_FOLDER := coqprime
 ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5
 else
 ifneq ($(PROFILE),)
-OTHERFLAGS ?= -profile-ltac -w "-deprecated-appcontext -notation-overridden"
+OTHERFLAGS ?= -profile-ltac -w "-notation-overridden"
 else
-OTHERFLAGS ?= -w "-deprecated-appcontext -notation-overridden"
+OTHERFLAGS ?= -w "-notation-overridden"
 endif
 endif
 
diff --git a/src/Compilers/EtaWf.v b/src/Compilers/EtaWf.v
index e8dd2f846..1134b5d05 100644
--- a/src/Compilers/EtaWf.v
+++ b/src/Compilers/EtaWf.v
@@ -28,7 +28,7 @@ Section language.
     | _ => progress split_iff
     | _ => rewrite eq_interp_flat_type_eta_gen by assumption
     | [ H : _ |- _ ] => rewrite eq_interp_flat_type_eta_gen in H by assumption
-    | [ H : appcontext[interp_flat_type_eta_gen] |- _ ]
+    | [ H : context[interp_flat_type_eta_gen] |- _ ]
       => setoid_rewrite eq_interp_flat_type_eta_gen in H; [ | assumption.. ]
     | _ => progress break_match
     | [ H : wff _ _ _ |- _ ] => solve [ inversion H ]
diff --git a/src/Compilers/ExprInversion.v b/src/Compilers/ExprInversion.v
index a1d2587f5..48ea30907 100644
--- a/src/Compilers/ExprInversion.v
+++ b/src/Compilers/ExprInversion.v
@@ -174,13 +174,13 @@ Ltac invert_expr := repeat invert_expr_step.
 
 Ltac invert_match_expr_step :=
   match goal with
-  | [ |- appcontext[match ?e with TT => _ | _ => _ end] ]
+  | [ |- context[match ?e with TT => _ | _ => _ end] ]
     => invert_one_expr e
-  | [ |- appcontext[match ?e with Abs _ _ _ => _ end] ]
+  | [ |- context[match ?e with Abs _ _ _ => _ end] ]
     => invert_one_expr e
-  | [ H : appcontext[match ?e with TT => _ | _ => _ end] |- _ ]
+  | [ H : context[match ?e with TT => _ | _ => _ end] |- _ ]
     => invert_one_expr e
-  | [ H : appcontext[match ?e with Abs _ _ _ => _ end] |- _ ]
+  | [ H : context[match ?e with Abs _ _ _ => _ end] |- _ ]
     => invert_one_expr e
   end.
 
diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v
index 9d3d8544b..810db4d9b 100644
--- a/src/Compilers/Reify.v
+++ b/src/Compilers/Reify.v
@@ -424,7 +424,7 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac :=
                   clear;
                   abstract (
                       lazymatch goal with
-                      | [ |- appcontext[@InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e] ]
+                      | [ |- context[@InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e] ]
                         => let interp_base_type' := (eval hnf in interp_base_type) in
                            let interp_op' := (eval hnf in interp_op) in
                            change interp_base_type with interp_base_type';
diff --git a/src/Compilers/Z/OpInversion.v b/src/Compilers/Z/OpInversion.v
index 58b00c538..e6fc3055b 100644
--- a/src/Compilers/Z/OpInversion.v
+++ b/src/Compilers/Z/OpInversion.v
@@ -19,9 +19,9 @@ Ltac invert_op := repeat invert_op_step.
 
 Ltac invert_match_op_step :=
   match goal with
-  | [ |- appcontext[match ?e with OpConst _ _ => _ | _ => _ end] ]
+  | [ |- context[match ?e with OpConst _ _ => _ | _ => _ end] ]
     => invert_one_op e
-  | [ H : appcontext[match ?e with OpConst _ _ => _ | _ => _ end] |- _ ]
+  | [ H : context[match ?e with OpConst _ _ => _ | _ => _ end] |- _ ]
     => invert_one_op e
   end.
 
diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v
index 8a38275dd..681f0b0a9 100644
--- a/src/LegacyArithmetic/Pow2BaseProofs.v
+++ b/src/LegacyArithmetic/Pow2BaseProofs.v
@@ -280,8 +280,8 @@ Section Pow2BaseProofs.
            | |- _ => rewrite nth_default_base
            | |- _ => rewrite IHi
            | |- _ => rewrite <-Z.lor_shiftl by (rewrite ?Z.pow2_mod_spec; try apply Z.mod_pos_bound; zero_bounds)
-           | |- appcontext[min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega)
-           | |- appcontext[2 ^ ?a * _] => rewrite (Z.mul_comm (2 ^ a)); rewrite <-Z.shiftl_mul_pow2
+           | |- context[min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega)
+           | |- context[2 ^ ?a * _] => rewrite (Z.mul_comm (2 ^ a)); rewrite <-Z.shiftl_mul_pow2
            | |- _ => solve [auto]
            | |- _ => lia
            end.
@@ -291,7 +291,7 @@ Section Pow2BaseProofs.
            | |- _ => progress autorewrite with Ztestbit
            | |- _ => rewrite Z.testbit_pow2_mod by (omega || trivial)
            | |- _ => break_if; try omega
-           | H : ?a < ?b |- appcontext[Z.testbit _ (?a - ?b)] =>
+           | H : ?a < ?b |- context[Z.testbit _ (?a - ?b)] =>
              rewrite (Z.testbit_neg_r _ (a-b)) by omega
            | |- _ => reflexivity
            | |- _ => solve [f_equal; ring]
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index a9987ffde..b49367600 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -252,7 +252,7 @@ Ltac boring :=
   simpl; intuition auto with zarith datatypes;
   repeat match goal with
            | [ H : _ |- _ ] => rewrite H; clear H
-           | [ |- appcontext[match ?pf with end] ] => solve [ case pf ]
+           | [ |- context[match ?pf with end] ] => solve [ case pf ]
            | _ => progress autounfold in *
            | _ => progress autorewrite with core
            | _ => progress simpl in *
@@ -633,7 +633,7 @@ Qed.
 (* grumble, grumble, [rewrite] is bad at inferring the identity function, and constant functions *)
 Ltac rewrite_rev_combine_update_nth :=
   let lem := match goal with
-             | [ |- appcontext[update_nth ?n (fun xy => (@?f xy, @?g xy)) (combine ?xs ?ys)] ]
+             | [ |- context[update_nth ?n (fun xy => (@?f xy, @?g xy)) (combine ?xs ?ys)] ]
                => let f := match (eval cbv [fst] in (fun y x => f (x, y))) with
                            | fun _ => ?f => f
                            end in
@@ -1564,10 +1564,10 @@ Qed.
 Local Hint Resolve map2_nil_r map2_nil_l.
 
 Ltac simpl_list_lengths := repeat match goal with
-                                  | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H
-                                  | H : appcontext[length (_ :: _)] |- _ => rewrite length_cons in H
-                                  | |- appcontext[length (@nil ?A)] => rewrite (@nil_length0 A)
-                                  | |- appcontext[length (_ :: _)] => rewrite length_cons
+                                  | H : context[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H
+                                  | H : context[length (_ :: _)] |- _ => rewrite length_cons in H
+                                  | |- context[length (@nil ?A)] => rewrite (@nil_length0 A)
+                                  | |- context[length (_ :: _)] => rewrite length_cons
                                   end.
 
 Section OpaqueMap2.
diff --git a/src/Util/Tactics/BreakMatch.v b/src/Util/Tactics/BreakMatch.v
index f03823a92..95a060750 100644
--- a/src/Util/Tactics/BreakMatch.v
+++ b/src/Util/Tactics/BreakMatch.v
@@ -70,31 +70,31 @@ Ltac destruct_rewrite_sumbool e :=
       end.
 Ltac break_match_step only_when :=
   match goal with
-  | [ |- appcontext[match ?e with _ => _ end] ]
+  | [ |- context[match ?e with _ => _ end] ]
     => only_when e; is_var e; destruct e
-  | [ |- appcontext[match ?e with _ => _ end] ]
+  | [ |- context[match ?e with _ => _ end] ]
     => only_when e;
        match type of e with
        | sumbool _ _ => destruct_rewrite_sumbool e
        end
-  | [ |- appcontext[if ?e then _ else _] ]
+  | [ |- context[if ?e then _ else _] ]
     => only_when e; destruct e eqn:?
-  | [ |- appcontext[match ?e with _ => _ end] ]
+  | [ |- context[match ?e with _ => _ end] ]
     => only_when e; destruct e eqn:?
   | _ => let v := fresh in set_match_refl v only_when; destruct_by_existing_equation v
   end.
 Ltac break_match_hyps_step only_when :=
   match goal with
-  | [ H : appcontext[match ?e with _ => _ end] |- _ ]
+  | [ H : context[match ?e with _ => _ end] |- _ ]
     => only_when e; is_var e; destruct e
-  | [ H : appcontext[match ?e with _ => _ end] |- _ ]
+  | [ H : context[match ?e with _ => _ end] |- _ ]
     => only_when e;
        match type of e with
        | sumbool _ _ => destruct_rewrite_sumbool e
        end
-  | [ H : appcontext[if ?e then _ else _] |- _ ]
+  | [ H : context[if ?e then _ else _] |- _ ]
     => only_when e; destruct e eqn:?
-  | [ H : appcontext[match ?e with _ => _ end] |- _ ]
+  | [ H : context[match ?e with _ => _ end] |- _ ]
     => only_when e; destruct e eqn:?
   | _ => let v := fresh in set_match_refl_hyp v only_when; destruct_by_existing_equation v
   end.
@@ -114,12 +114,12 @@ Ltac break_match_when_head T := repeat break_match_when_head_step T.
 Ltac break_match_hyps_when_head T := repeat break_match_hyps_when_head_step T.
 Ltac break_innermost_match_step :=
   break_match_step ltac:(fun v => lazymatch v with
-                                  | appcontext[match _ with _ => _ end] => fail
+                                  | context[match _ with _ => _ end] => fail
                                   | _ => idtac
                                   end).
 Ltac break_innermost_match_hyps_step :=
   break_match_hyps_step ltac:(fun v => lazymatch v with
-                                       | appcontext[match _ with _ => _ end] => fail
+                                       | context[match _ with _ => _ end] => fail
                                        | _ => idtac
                                        end).
 Ltac break_innermost_match := repeat break_innermost_match_step.
diff --git a/src/Util/Tactics/Contains.v b/src/Util/Tactics/Contains.v
index aa4fddac2..0ee6116e3 100644
--- a/src/Util/Tactics/Contains.v
+++ b/src/Util/Tactics/Contains.v
@@ -2,12 +2,12 @@
 Ltac contains search_for in_term :=
   idtac;
   lazymatch in_term with
-  | appcontext[search_for] => idtac
+  | context[search_for] => idtac
   end.
 
 Ltac free_in x y :=
   idtac;
   match y with
-    | appcontext[x] => fail 1 x "appears in" y
+    | context[x] => fail 1 x "appears in" y
     | _ => idtac
   end.
diff --git a/src/Util/Tactics/Revert.v b/src/Util/Tactics/Revert.v
index 5f549025d..78c94f956 100644
--- a/src/Util/Tactics/Revert.v
+++ b/src/Util/Tactics/Revert.v
@@ -3,8 +3,8 @@ Ltac revert_last_nondep :=
   match goal with
   | [ H : _ |- _ ]
     => lazymatch goal with
-       | [ H' : appcontext[H] |- _ ] => fail
-       | [ |- appcontext[H] ] => fail
+       | [ H' : context[H] |- _ ] => fail
+       | [ |- context[H] ] => fail
        | _ => idtac
        end;
        revert H
diff --git a/src/Util/Tactics/SetEvars.v b/src/Util/Tactics/SetEvars.v
index 471d61f60..b55f0edb1 100644
--- a/src/Util/Tactics/SetEvars.v
+++ b/src/Util/Tactics/SetEvars.v
@@ -1,4 +1,4 @@
 Ltac set_evars :=
   repeat match goal with
-         | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
+         | [ |- context[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
          end.
diff --git a/src/Util/Tactics/SimplifyProjections.v b/src/Util/Tactics/SimplifyProjections.v
index f9b319057..bf9f2d347 100644
--- a/src/Util/Tactics/SimplifyProjections.v
+++ b/src/Util/Tactics/SimplifyProjections.v
@@ -8,7 +8,7 @@ Ltac pre_simplify_projection proj proj' uproj' :=
 Ltac do_simplify_projection_2Targ_4carg_step proj proj' uproj' construct :=
   change proj' with uproj' at 1;
   lazymatch goal with
-  | [ |- appcontext[uproj' _ _ (construct _ _ _ _)] ]
+  | [ |- context[uproj' _ _ (construct _ _ _ _)] ]
     => cbv beta iota delta [uproj']
   | _ => change uproj' with proj
   end.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 839defb03..4b19d5f8b 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -953,7 +953,7 @@ Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordTo
 Proof.
   unfold wfirstn.
   intros; rewrite wordToNat_split1.
-  match goal with |- appcontext[match ?x with _ => _ end] => generalize x end.
+  match goal with |- context[match ?x with _ => _ end] => generalize x end.
   intro H'; destruct H'.
   reflexivity.
 Qed.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index ed09bf828..07466154c 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -251,10 +251,10 @@ Ltac comes_before ls x y :=
   end.
 Ltac canonicalize_comm_step mul ls comm comm3 :=
   match goal with
-  | [ |- appcontext[mul ?x ?y] ]
+  | [ |- context[mul ?x ?y] ]
     => comes_before ls y x;
        rewrite (comm x y)
-  | [ |- appcontext[mul ?x (mul ?y ?z)] ]
+  | [ |- context[mul ?x (mul ?y ?z)] ]
     => comes_before ls y x;
        rewrite (comm3 x y z)
   end.
@@ -437,7 +437,7 @@ Module Z.
     intros; cbv [Z.pow2_mod].
     apply Z.bits_inj'; intros.
     repeat progress (try break_match; autorewrite with Ztestbit zsimplify; try reflexivity).
-    try match goal with H : ?a < ?b |- appcontext[Z.testbit _ (?a - ?b)] =>
+    try match goal with H : ?a < ?b |- context[Z.testbit _ (?a - ?b)] =>
       rewrite !Z.testbit_neg_r with (n := a - b) by omega end.
     autorewrite with Ztestbit; reflexivity.
   Qed.
@@ -2235,7 +2235,7 @@ Module Z.
            | |- _ => progress intros
            | |- _ => progress rewrite ?Z.eqb_eq, ?Z.eqb_neq in *
            | |- _ => progress autorewrite with Ztestbit
-           | |- appcontext[Z.eqb ?a ?b] => case_eq (Z.eqb a b)
+           | |- context[Z.eqb ?a ?b] => case_eq (Z.eqb a b)
            | |- _ => reflexivity || omega
            end.
   Qed.