diff --git a/prelude/option.v b/prelude/option.v
index 2dee5a724d29f0241a8344a1249df3802f37cdc2..5557f2ac63be245e2a0a452b825d5eaaecbfaf2d 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -298,11 +298,11 @@ End union_intersection_difference.
 (** * Tactics *)
 Tactic Notation "case_option_guard" "as" ident(Hx) :=
   match goal with
-  | H : appcontext C [@mguard option _ ?P ?dec] |- _ =>
+  | H : context C [@mguard option _ ?P ?dec] |- _ =>
     change (@mguard option _ P dec) with (λ A (f : P → option A),
       match @decide P dec with left H' => f H' | _ => None end) in *;
     destruct_decide (@decide P dec) as Hx
-  | |- appcontext C [@mguard option _ ?P ?dec] =>
+  | |- context C [@mguard option _ ?P ?dec] =>
     change (@mguard option _ P dec) with (λ A (f : P → option A),
       match @decide P dec with left H' => f H' | _ => None end) in *;
     destruct_decide (@decide P dec) as Hx
@@ -326,9 +326,9 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
       assert (mx = Some x') as H by tac
     | assert (mx = None) as H by tac ]
   in repeat match goal with
-  | H : appcontext [@mret _ _ ?A] |- _ =>
+  | H : context [@mret _ _ ?A] |- _ =>
      change (@mret _ _ A) with (@Some A) in H
-  | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
+  | |- context [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
   | H : context [mbind (M:=option) (A:=?A) ?f ?mx] |- _ =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
   | H : context [fmap (M:=option) (A:=?A) ?f ?mx] |- _ =>
diff --git a/prelude/tactics.v b/prelude/tactics.v
index c55f53d667bbf3f8d2765f35bd431e48131eab48..08cb953fef6db5663dfeb8b4e6b2839d6bbbdeaa 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -158,7 +158,7 @@ Coq-club message:
 https://sympa.inria.fr/sympa/arc/coq-club/2012-10/msg00147.html *)
 Ltac fold_classes :=
   repeat match goal with
-  | |- appcontext [ ?F ] =>
+  | |- context [ ?F ] =>
     progress match type of F with
     | FMap _ =>
        change F with (@fmap _ F);
@@ -176,7 +176,7 @@ Ltac fold_classes :=
   end.
 Ltac fold_classes_hyps H :=
   repeat match type of H with
-  | appcontext [ ?F ] =>
+  | context [ ?F ] =>
     progress match type of F with
     | FMap _ =>
        change F with (@fmap _ F) in H;