diff --git a/ProofMode.md b/ProofMode.md
index dbbe030f4356c58bbb2452006c566fa0989e5abf..d178f52f0abc8ca80f3c8cb45949df86ea59cb22 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -198,9 +198,9 @@ _introduction patterns_:
 Apart from this, there are the following introduction patterns that can only
 appear at the top level:
 
-- `{H1 ... Hn}` : clear `H1 ... Hn`.
-- `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
-  previous pattern, e.g., `{$H1 H2 $H3}`).
+- `{selpat}` : clear the hypotheses given by the selection pattern `selpat`.
+  Items of the selection pattern can be prefixed with `$`, which cause them to
+  be framed instead of cleared.
 - `!%` : introduce a pure goal (and leave the proof mode).
 - `!#` : introduce an always modality and clear the spatial context.
 - `!>` : introduce a modality.
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 39a28f98b8a6c7772a7f31ecc1e67535ffea57e1..7d1c308a4d5cb15c612fc21f1ee40456a218ff43 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -1,5 +1,5 @@
 From stdpp Require Export strings.
-From iris.proofmode Require Import tokens.
+From iris.proofmode Require Import tokens sel_patterns.
 Set Default Proof Using "Type".
 
 Inductive intro_pat :=
@@ -18,8 +18,8 @@ Inductive intro_pat :=
   | IDone : intro_pat
   | IForall : intro_pat
   | IAll : intro_pat
-  | IClear : string → intro_pat
-  | IClearFrame : string → intro_pat.
+  | IClear : sel_pat → intro_pat
+  | IClearFrame : sel_pat → intro_pat.
 
 Module intro_pat.
 Inductive stack_item :=
@@ -96,8 +96,14 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   end
 with parse_clear (ts : list token) (k : stack) : option stack :=
   match ts with
-  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame s) :: k)
-  | TName s :: ts => parse_clear ts (SPat (IClear s) :: k)
+  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelName s)) :: k)
+  | TFrame :: TPure :: ts => parse_clear ts (SPat (IClearFrame SelPure) :: k)
+  | TFrame :: TAlways :: ts => parse_clear ts (SPat (IClearFrame SelPersistent) :: k)
+  | TFrame :: TSep :: ts => parse_clear ts (SPat (IClearFrame SelSpatial) :: k)
+  | TName s :: ts => parse_clear ts (SPat (IClear (SelName s)) :: k)
+  | TPure :: ts => parse_clear ts (SPat (IClear SelPure) :: k)
+  | TAlways :: ts => parse_clear ts (SPat (IClear SelPersistent) :: k)
+  | TSep :: ts => parse_clear ts (SPat (IClear SelSpatial) :: k)
   | TBraceR :: ts => parse_go ts k
   | _ => None
   end.
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index 01581650c0bd18ac0bc3afb9f9517f1731251cda..5578d17e222562e2b933cd9532cb7097223f86f4 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -30,6 +30,7 @@ Definition parse (s : string) : option (list sel_pat) :=
 
 Ltac parse s :=
   lazymatch type of s with
+  | sel_pat => constr:([s])
   | list sel_pat => s
   | list string => eval vm_compute in (SelName <$> s)
   | string =>