diff --git a/CHANGELOG.md b/CHANGELOG.md
index 082fded0de58e8490894ac2d66b75d816e5d59d4..5b13a2243c791e2df60b330fe69b55c439ca56f6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -156,7 +156,7 @@ s/\blist_singletonM_included\b/list_singleton_included/g
   - quantifiers[†]: `forall` for `∀` and `exists` for `∃`
   - separation logic: `**` for `∗`, `-*` for `-∗`, and `*-*` for `∗-∗`
   - step indexing: `|>` for `â–·`
-  - modalities: `<intuit>` for `â–¡` and `<except_0>` for `â—‡`
+  - modalities: `<#>` for `â–¡` and `<except_0>` for `â—‡`
   - most derived notations can be computed from previous notations using the
     substitutions above, e.g. replace `∗` with `*` and `▷` with `|>`. Examples
     include the following:
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index d4c55b7de75ad0f43c7f0bc07f96284c3f54c904..1c55fd9385cf8ca0687807110b939683d991e232 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -11,10 +11,10 @@ Section base_logic_tests.
   Lemma test_random_stuff (P1 P2 P3 : nat -> uPred M) :
     |-- forall (x y : nat) a b,
       x ≡ y ->
-      <intuit> (uPred_ownM (a â‹… b) -*
-      (exists y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ <intuit> uPred_ownM c) -*
-      <intuit> |> (forall z, P2 z ∨ True -> P2 z) -*
-      |> (forall n m : nat, P1 n -> <intuit> (True ∧ P2 n -> <intuit> (⌜n = n⌝ ↔ P3 n))) -*
+      <#> (uPred_ownM (a â‹… b) -*
+      (exists y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ <#> uPred_ownM c) -*
+      <#> |> (forall z, P2 z ∨ True -> P2 z) -*
+      |> (forall n m : nat, P1 n -> <#> (True ∧ P2 n -> <#> (⌜n = n⌝ ↔ P3 n))) -*
       |> ⌜x = 0⌝ \/ exists x z, |> P3 (x + z) ** uPred_ownM b ** uPred_ownM (core b)).
   Proof.
     iIntros (i [|j] a b ?) "!> [Ha Hb] H1 #H2 H3"; setoid_subst.
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 725f06a14f7d51741c84ddeb9d86a7b4804b0c30..77781344ad1ca0fc96d990e6dc25792791ad95f7 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -50,8 +50,8 @@ Notation "P <-> Q" := (P ↔ Q)%I (at level 95, no associativity, only parsing)
 
 Notation "P *-* Q" := (P ∗-∗ Q)%I (at level 95, no associativity, only parsing) : bi_scope.
 
-Notation "'<intuit>' P" := (â–¡ P)%I (at level 20, right associativity, only parsing) : bi_scope.
-Notation "'<intuit>?' p P" := (â–¡?p P)%I (at level 20, p at level 9, P at level 20,
+Notation "'<#>' P" := (â–¡ P)%I (at level 20, right associativity, only parsing) : bi_scope.
+Notation "'<#>?' p P" := (â–¡?p P)%I (at level 20, p at level 9, P at level 20,
    right associativity, only parsing) : bi_scope.
 
 Notation "'<except_0>' P" := (â—‡ P)%I (at level 20, right associativity, only parsing) : bi_scope.