s/appcontext/context/

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

5 files changed, 16 insertions, 16 deletions

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.