diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 791ef2d3008d877d0938f2721265e2f5fdb96b8d..b51728b509157fa9cd9600a8cb40b379a8505465 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -1532,7 +1532,7 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
   repeat match goal with
   | _ => progress simpl_map by tac
   | _ => progress simplify_equality
-  | _ => progress simpl_option_monad by tac
+  | _ => progress simpl_option by tac
   | H : {[ _ ↦ _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H
   | H : {[ _ ↦ _ ]} !! _ = Some _ |- _ =>
     rewrite lookup_singleton_Some in H; destruct H
diff --git a/prelude/option.v b/prelude/option.v
index 08bc2bc6b6b84bf78a2f0a3590c4c228f55f761f..237194c24b6f92f723b568097ab8e72b4d4217a9 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -261,7 +261,7 @@ Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (x : option A) :
   (P ↔ Q) → guard P; x = guard Q; x.
 Proof. intros [??]. repeat case_option_guard; intuition. Qed.
 
-Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
+Tactic Notation "simpl_option" "by" tactic3(tac) :=
   let assert_Some_None A o H := first
     [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
       assert (o = Some x') as H by tac
@@ -308,7 +308,7 @@ Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
 Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
   repeat match goal with
   | _ => progress simplify_equality'
-  | _ => progress simpl_option_monad by tac
+  | _ => progress simpl_option by tac
   | _ : maybe _ ?x = Some _ |- _ => is_var x; destruct x
   | _ : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
   | _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x