diff --git a/ProofMode.md b/ProofMode.md
index a1507dfba484b0b006f12fb373b83a55a9b11c33..79eca351adb88f8f172f66ea6397f4f4899dceb0 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -242,12 +242,10 @@ _specification patterns_ to express splitting of hypotheses:
   consumed. Hypotheses may be prefixed with a `$`, which results in them being
   framed in the generated goal for the premise.
 - `[-H1 ... Hn]` : negated form of the above pattern.
-- `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
+- `[> H1 ... Hn]` : same as the above pattern, but can only be used if the goal
   is a modality, in which case the modality will be kept in the generated goal
   for the premise will be wrapped into the modality.
-- `>[-H1 ... Hn]`  : negated form of the above pattern.
-- `>` : shorthand for `>[-]` (typically used for the last premise of an applied
-  lemma).
+- `[> -H1 ... Hn]`  : negated form of the above pattern.
 - `[#]` : This pattern can be used when eliminating `P -∗ Q` with `P` being
   persistent. Using this pattern, all hypotheses are available in the goal for
   `P`, as well the remaining goal. The pattern can optionally contain 
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 0722ee82331455c7c85cf8da7d4ecec0cf1caa6c..413fbdd5de31c44a0b45aa0a3eed58f1e8fed538 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -225,7 +225,7 @@ Lemma box_empty E f P :
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iAssert ([∗ map] γ↦b ∈ f, ▷ Φ γ ∗ box_own_auth γ (◯ Excl' false) ∗
-    box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]".
+    box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
   { iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
     iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (true = b) as <- by eauto.
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index 2bdce5c36927376aa33c3c4e64a3f29413175da7..d06424595a0662baf2ca43593fca19603e348f0e 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -93,7 +93,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
 Proof.
   iIntros (Φ) "HΦ".
   rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
-  iApply ("HΦ" with ">[-]").
+  iApply ("HΦ" with "[> -]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
   iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
     as (γ') "[#? Hγ']"; eauto.
@@ -102,7 +102,7 @@ Proof.
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { done. }
   iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
-    ∗ sts_ownS γ' low_states {[Send]})%I with ">[-]" as "[Hr Hs]".
+    ∗ sts_ownS γ' low_states {[Send]})%I with "[> -]" as "[Hr Hs]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     - set_solver.
     - iApply (sts_own_weaken with "Hγ'");
@@ -140,7 +140,7 @@ Proof.
   wp_load. destruct p.
   - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
     { iSplit; first done. rewrite /barrier_inv /=. by iFrame. }
-    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ".
+    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[> Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
     iModIntro. wp_if.
     iApply ("IH" with "Hγ [HQR] [HΦ]"); auto.
@@ -175,7 +175,7 @@ Proof.
     rewrite /barrier_inv /=. iNext. iFrame "Hl".
     by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
   iAssert (sts_ownS γ (i_states i1) {[Change i1]}
-    ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".
+    ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with "[> -]" as "[Hγ1 Hγ2]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     - abstract set_solver.
     - iApply (sts_own_weaken with "Hγ");
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 03b61878d0e033cffe79f1a491f352036f15c17c..007063e76dd1d5f9a39ba7e93e030b6438a7e2e6 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -129,7 +129,7 @@ Lemma wp_strong_mono E1 E2 e Φ Ψ :
 Proof.
   iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
-  { iApply ("HΦ" with ">[-]"). by iApply (fupd_mask_mono E1 _). }
+  { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
   iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 92c215d55608589ed51b93399e16d570b052ff53..691ba64d586d36fd621abf7b1fa22b1fe374e97a 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -41,14 +41,13 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
      parse_go ts (SAutoFrame GPersistent :: k)
   | TBracketL :: TFrame :: TBracketR :: ts =>
      parse_go ts (SAutoFrame GSpatial :: k)
-  | TModal :: TBracketL :: TFrame :: TBracketR :: ts =>
+  | TBracketL :: TModal :: TFrame :: TBracketR :: ts =>
      parse_go ts (SAutoFrame GModal :: k)
   | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SPureGoal false :: k)
   | TBracketL :: TPure :: TDone :: TBracketR :: ts => parse_go ts (SPureGoal true :: k)
   | TBracketL :: TAlways :: ts => parse_goal ts GPersistent false [] [] k
+  | TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
   | TBracketL :: ts => parse_goal ts GSpatial false [] [] k
-  | TModal :: TBracketL :: ts => parse_goal ts GModal false [] [] k
-  | TModal :: ts => parse_go ts (SGoal (SpecGoal GModal true [] [] false) :: k)
   | TForall :: ts => parse_go ts (SForall :: k)
   | _ => None
   end
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 13a85e4c5a0c113e5593dd3dc0e0ec6ee5b3ad69..c3a00b51cb7b0221698108c1ad5c200471c8b7f6 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -96,7 +96,7 @@ Section iris.
     (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.
   Proof.
     iIntros (?) "H HP HQ".
-    iApply ("H" with "[% //] HP >[HQ] >[//]").
+    iApply ("H" with "[% //] [$] [> HQ] [> //]").
     by iApply inv_alloc.
   Qed.
 End iris.
@@ -124,7 +124,7 @@ Lemma demo_12 (M : ucmraT) (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
 
 Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) -∗ |==> P.
-Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed.
+Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
 
 Lemma demo_14 (M : ucmraT) (P : uPred M) : False -∗ P.
 Proof. iIntros "H". done. Qed.