s/appcontext/context/

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

4 files changed, 8 insertions, 8 deletions

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.