diff --git a/ProofMode.md b/ProofMode.md
index 072c66c7252c4b34f90c354dee484d4fce8758de..6e2c229704098f2dd4fb118df7d323b216f46886 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -203,6 +203,8 @@ appear at the top level:
 - `!#` : introduce an always modality (given that the spatial context is empty).
 - `!>` : introduce a modality.
 - `/=` : perform `simpl`.
+- `//` : perform `try done` on all goals.
+- `//=` : syntactic sugar for `/= //`
 - `*` : introduce all universal quantifiers.
 - `**` : introduce all universal quantifiers, as well as all arrows and wands.
 
@@ -235,30 +237,52 @@ _specification patterns_ to express splitting of hypotheses:
 
 - `H` : use the hypothesis `H` (it should match the premise exactly). If `H` is
   spatial, it will be consumed.
-- `[H1 ... Hn]` : generate a goal with the (spatial) hypotheses `H1 ... Hn` and
-  all persistent hypotheses. The spatial hypotheses among `H1 ... Hn` will be
-  consumed. Hypotheses may be prefixed with a `$`, which results in them being
-  framed in the generated goal.
-- `[-H1 ... Hn]` : negated form of the above pattern.
-- `>[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).
-- `[#]` : This pattern can be used when eliminating `P -∗ Q` with `P`
-  persistent. Using this pattern, all hypotheses are available in the goal for
-  `P`, as well the remaining goal.
-- `[%]` : This pattern can be used when eliminating `P -∗ Q` when `P` is pure.
-  It will generate a Coq goal for `P` and does not consume any hypotheses.
+
+- `[H1 .. Hn]` and `[H1 .. Hn //]` : generate a goal for the premise with the
+  (spatial) hypotheses `H1 ... Hn` and all persistent hypotheses. The spatial
+  hypotheses among `H1 ... Hn` will be consumed, and will not be available for
+  subsequent goals. Hypotheses prefixed with a `$` will be framed in the
+  goal for the premise. The pattern can be terminated with a `//`, which causes
+  `done` to be called to close the goal (after framing).
+- `[-H1 ... Hn]` and `[-H1 ... Hn //]` : the negated forms of the above
+  patterns, where the goal for the premise will have all spatial premises except
+  `H1 .. Hn`.
+
+- `[> H1 ... Hn]` and `[> H1 ... Hn //]` : like the above patterns, but these
+  patterns can only be used if the goal is a modality `M`, in which case
+  the goal for the premise will be wrapped in the modality `M`.
+- `[> -H1 ... Hn]` and `[> -H1 ... Hn //]` : the negated forms of the above
+  patterns.
+
+- `[# $H1 .. $Hn]` and `[# $H1 .. $Hn //]` : generate a goal for a persistent
+  premise in which all hypotheses are available. This pattern does not consume
+  any hypotheses; all hypotheses are available in the goal for the premise, as
+  well in the subsequent goal. The hypotheses `$H1 ... $Hn` will be framed in
+  the goal for the premise. These patterns can be terminated with a `//`, which
+  causes `done` to be called to close the goal (after framing).
+- `[%]` and `[% //]` : generate a Coq goal for a pure premise. This pattern
+  does not consume any hypotheses. The pattern can be terminated with a `//`,
+  which causes `done` to be called to close the goal.
+
+- `[$]` : solve the premise by framing. It will first repeatedly frame the
+  spatial hypotheses, and then repeatedly frame the persistent hypotheses.
+  Spatial hypothesis that are not framed are carried over to the subsequent
+  goal.
+- `[> $]` : like the above pattern, but this pattern can only be used if the
+  goal is a modality `M`, in which case the goal for the premise will be wrapped
+  in the modality `M` before framing.
+- `[# $]` : solve the persistent premise by framing. It will first repeatedly
+  frame the spatial hypotheses, and then repeatedly frame the persistent
+  hypotheses. This pattern does not consume any hypotheses.
 
 For example, given:
 
-        H : □ P -∗ P 2 -∗ x = 0 -∗ Q1 ∗ Q2
+        H : □ P -∗ P 2 -∗ R -∗ x = 0 -∗ Q1 ∗ Q2
+
+One can write:
 
-You can write:
+        iDestruct ("H" with "[#] [H1 $H2] [$] [% //]") as "[H4 H5]".
 
-        iDestruct ("H" with "[#] [H1 H2] [%]") as "[H4 H5]".
 
 Proof mode terms
 ================
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/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index fe5e8da94ee7310e5ba34578ede8881ea35f50ad..ced2ab68ca2612b5d995e29799a53f8728df7e6b 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -104,7 +104,7 @@ Qed.
 Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup I i P with "[$Hw $Hi]") as (Q) "[% #HPQ]".
+  iDestruct (invariant_lookup I i P with "[$]") as (Q) "[% #HPQ]".
   iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
     iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
@@ -114,9 +114,9 @@ Qed.
 Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ ownE {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup with "[$Hw $Hi]") as (Q) "[% #HPQ]".
+  iDestruct (invariant_lookup with "[$]") as (Q) "[% #HPQ]".
   iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
-  - iDestruct (ownD_singleton_twice with "[-]") as %[]. by iFrame.
+  - iDestruct (ownD_singleton_twice with "[$]") as %[].
   - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
 Qed.
@@ -127,7 +127,7 @@ Lemma ownI_alloc φ P :
 Proof.
   iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
   iMod (own_empty (gset_disjUR positive) disabled_name) as "HE".
-  iMod (own_updateP with "HE") as "HE".
+  iMod (own_updateP with "[$]") as "HE".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
     intros E. destruct (Hfresh (E ∪ dom _ I))
       as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
@@ -149,7 +149,7 @@ Lemma ownI_alloc_open φ P :
 Proof.
   iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
   iMod (own_empty (gset_disjUR positive) disabled_name) as "HD".
-  iMod (own_updateP with "HD") as "HD".
+  iMod (own_updateP with "[$]") as "HD".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
     intros E. destruct (Hfresh (E ∪ dom _ I))
       as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); 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 2e5428ddc1d807cb7a247df4801be0fbf500565f..007063e76dd1d5f9a39ba7e93e030b6438a7e2e6 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -129,11 +129,11 @@ 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" $! σ1 with "Hσ") as "[$ H]".
+  iMod ("H" with "[$]") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
+  iMod ("H" with "[//]") as "($ & H & $)"; auto.
   iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
 Qed.
 
@@ -155,10 +155,10 @@ Proof.
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" with "[]") as "(Hphy & H & $)"; first done.
+  iMod ("H" with "[//]") as "(Hphy & H & $)".
   rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
-  - iDestruct "H" as ">> $". iFrame. eauto.
-  - iMod ("H" with "Hphy") as "[H _]".
+  - iDestruct "H" as ">> $". eauto with iFrame.
+  - iMod ("H" with "[$]") as "[H _]".
     iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hatomic _ _ _ _ Hstep).
 Qed.
 
@@ -167,9 +167,9 @@ Lemma wp_step_fupd E1 E2 e P Φ :
   (|={E1,E2}▷=> P) -∗ WP e @ E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
-  iIntros (σ1) "Hσ". iMod "HR". iMod ("H" $! _ with "Hσ") as "[$ H]".
+  iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
   iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
-  iMod ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
+  iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
   iMod "HR". iModIntro. iApply (wp_strong_mono E2); first done.
   iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
 Qed.
@@ -181,11 +181,11 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by iApply fupd_wp. }
   rewrite wp_unfold /wp_pre fill_not_val //.
-  iIntros (σ1) "Hσ". iMod ("H" $! _ with "Hσ") as "[% H]". iModIntro; iSplit.
+  iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
   { iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
   iNext; iIntros (e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
-  iMod ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
+  iMod ("H" $! e2' σ2 efs with "[//]") as "($ & H & $)".
   by iApply "IH".
 Qed.
 
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index fb5f25e0515068749a97ccda4c8d1b74d6afd745..1e2905b422155af638a8ce7b586d00395f2b0096 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -573,6 +573,24 @@ Proof.
   by rewrite always_if_elim assoc !wand_elim_r.
 Qed.
 
+Lemma tac_unlock P Q : (P ⊢ Q) → P ⊢ locked Q.
+Proof. by unlock. Qed.
+
+Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
+  envs_lookup_delete j Δ = Some (q, R, Δ') →
+  IntoWand R P1 P2 →
+  ElimModal P1' P1 Q Q →
+  (Δ' ⊢ P1' ∗ locked Q') →
+  Q' = (P2 -∗ Q)%I →
+  Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
+  rewrite envs_lookup_sound //. rewrite HPQ -lock.
+  rewrite (into_wand R) assoc -(comm _ P1') -assoc always_if_elim.
+  rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
+  by rewrite assoc !wand_elim_r.
+Qed.
+
 Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
   IntoWand R P1 P2 → FromPure P1 φ →
@@ -643,14 +661,23 @@ Qed.
 Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
   envs_split lr js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ = Some Δ' →
-  (Δ1 ⊢ P) → PersistentP P →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  PersistentP P →
+  (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ?? HP ? <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
+  intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
   rewrite HP sep_elim_l (always_and_sep_l P) envs_app_sound //; simpl.
   by rewrite right_id wand_elim_r.
 Qed.
 
+Lemma tac_assert_pure Δ Δ' j P φ Q :
+  envs_app false (Esnoc Enil j P) Δ = Some Δ' →
+  FromPure P φ →
+  φ → (Δ' ⊢ Q) → Δ ⊢ Q.
+Proof.
+  intros ??? <-. rewrite envs_app_sound //; simpl.
+  by rewrite right_id -(from_pure P) pure_True // -always_impl_wand True_impl.
+Qed.
+
 Lemma tac_pose_proof Δ Δ' j P Q :
   P →
   envs_app true (Esnoc Enil j P) Δ = Some Δ' →
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 84af8d27136f1b044da22ef708b272421dbd15e1..2a6cac32110db49e9e4a119ca2b392904c8ce71e 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -15,6 +15,7 @@ Inductive intro_pat :=
   | IAlwaysIntro : intro_pat
   | IModalIntro : intro_pat
   | ISimpl : intro_pat
+  | IDone : intro_pat
   | IForall : intro_pat
   | IAll : intro_pat
   | IClear : string → intro_pat
@@ -87,6 +88,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
   | TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k)
   | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
+  | TDone :: ts => parse_go ts (SPat IDone :: k)
   | TAll :: ts => parse_go ts (SPat IAll :: k)
   | TForall :: ts => parse_go ts (SPat IForall :: k)
   | TBraceL :: ts => parse_clear ts k
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index be72220b4bb97b672452c95fd65b90cd1562bdca..691ba64d586d36fd621abf7b1fa22b1fe374e97a 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -2,22 +2,31 @@ From stdpp Require Export strings.
 From iris.proofmode Require Import tokens.
 Set Default Proof Using "Type".
 
+Inductive goal_kind := GSpatial | GModal | GPersistent.
+
 Record spec_goal := SpecGoal {
-  spec_goal_modal : bool;
+  spec_goal_kind : goal_kind;
   spec_goal_negate : bool;
   spec_goal_frame : list string;
-  spec_goal_hyps : list string
+  spec_goal_hyps : list string;
+  spec_goal_done : bool
 }.
 
 Inductive spec_pat :=
-  | SGoal : spec_goal → spec_pat
-  | SGoalPersistent : spec_pat
-  | SGoalPure : spec_pat
+  | SForall : spec_pat
   | SName : string → spec_pat
-  | SForall : spec_pat.
+  | SPureGoal : bool → spec_pat
+  | SGoal : spec_goal → spec_pat
+  | SAutoFrame : goal_kind → spec_pat.
 
+Definition goal_kind_modal (k : goal_kind) : bool :=
+  match k with GModal => true | _ => false end.
 Definition spec_pat_modal (p : spec_pat) : bool :=
-  match p with SGoal g => spec_goal_modal g | _ => false end.
+  match p with
+  | SGoal g => goal_kind_modal (spec_goal_kind g)
+  | SAutoFrame k => goal_kind_modal k
+  | _ => false
+  end.
 
 Module spec_pat.
 Inductive state :=
@@ -28,30 +37,33 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
   match ts with
   | [] => Some (reverse k)
   | TName s :: ts => parse_go ts (SName s :: k)
-  | TBracketL :: TAlways :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
-  | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
-  | TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k
-  | TModal :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
-  | TModal :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
+  | TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
+     parse_go ts (SAutoFrame GPersistent :: k)
+  | TBracketL :: TFrame :: TBracketR :: ts =>
+     parse_go ts (SAutoFrame GSpatial :: k)
+  | 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
   | TForall :: ts => parse_go ts (SForall :: k)
   | _ => None
   end
-with parse_goal (ts : list token) (g : spec_goal)
+with parse_goal (ts : list token)
+    (ki : goal_kind) (neg : bool) (frame hyps : list string)
     (k : list spec_pat) : option (list spec_pat) :=
   match ts with
   | TMinus :: ts =>
-     guard (¬spec_goal_negate g ∧ spec_goal_frame g = [] ∧ spec_goal_hyps g = []);
-     parse_goal ts (SpecGoal (spec_goal_modal g) true
-       (spec_goal_frame g) (spec_goal_hyps g)) k
-  | TName s :: ts =>
-     parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
-       (spec_goal_frame g) (s :: spec_goal_hyps g)) k
-  | TFrame :: TName s :: ts =>
-     parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
-       (s :: spec_goal_frame g) (spec_goal_hyps g)) k
+     guard (¬neg ∧ frame = [] ∧ hyps = []);
+     parse_goal ts ki true frame hyps k
+  | TName s :: ts => parse_goal ts ki neg frame (s :: hyps) k
+  | TFrame :: TName s :: ts => parse_goal ts ki neg (s :: frame) hyps k
+  | TDone :: TBracketR :: ts =>
+     parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
   | TBracketR :: ts =>
-     parse_go ts (SGoal (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
-       (reverse (spec_goal_frame g)) (reverse (spec_goal_hyps g))) :: k)
+     parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) false) :: k)
   | _ => None
   end.
 Definition parse (s : string) : option (list spec_pat) :=
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 625970eee44ebcdd6e1004ede6e9e8cbdeb3cf20..3c13cf25f2d59cdbdcf90264faceac5396334b91 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -261,6 +261,72 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
     constr(t5) constr(t6) constr(t7) constr(t8)")" constr(Hs) :=
   iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ) Hs.
 
+(** * Basic introduction tactics *)
+Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
+  try iStartProof;
+  try first
+    [(* (∀ _, _) *) apply tac_forall_intro
+    |(* (?P → _) *) eapply tac_impl_intro_pure;
+      [let P := match goal with |- IntoPure ?P _ => P end in
+       apply _ || fail "iIntro:" P "not pure"|]
+    |(* (?P -∗ _) *) eapply tac_wand_intro_pure;
+      [let P := match goal with |- IntoPure ?P _ => P end in
+       apply _ || fail "iIntro:" P "not pure"|]
+    |(* ⌜∀ _, _⌝ *) apply tac_pure_forall_intro
+    |(* ⌜_ → _⌝ *) apply tac_pure_impl_intro];
+  intros x.
+
+Local Tactic Notation "iIntro" constr(H) :=
+  iStartProof;
+  first
+  [ (* (?Q → _) *)
+    eapply tac_impl_intro with _ H; (* (i:=H) *)
+      [reflexivity || fail 1 "iIntro: introducing" H
+                             "into non-empty spatial context"
+      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
+  | (* (_ -∗ _) *)
+    eapply tac_wand_intro with _ H; (* (i:=H) *)
+      [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
+  | fail 1 "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntro" "#" constr(H) :=
+  iStartProof;
+  first
+  [ (* (?P → _) *)
+    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
+      [let P := match goal with |- IntoPersistentP ?P _ => P end in
+       apply _ || fail 1 "iIntro: " P " not persistent"
+      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
+  | (* (?P -∗ _) *)
+    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
+      [let P := match goal with |- IntoPersistentP ?P _ => P end in
+       apply _ || fail 1 "iIntro: " P " not persistent"
+      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
+  | fail 1 "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntro" "_" :=
+  try iStartProof;
+  first
+  [ (* (?Q → _) *) apply tac_impl_intro_drop
+  | (* (_ -∗ _) *) apply tac_wand_intro_drop
+  | (* (∀ _, _) *) iIntro (_)
+  | fail 1 "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntroForall" :=
+  try iStartProof;
+  lazymatch goal with
+  | |- ∀ _, ?P => fail
+  | |- ∀ _, _ => intro
+  | |- _ ⊢ (∀ x : _, _) => let x' := fresh x in iIntro (x')
+  end.
+Local Tactic Notation "iIntro" :=
+  try iStartProof;
+  lazymatch goal with
+  | |- _ → ?P => intro
+  | |- _ ⊢ (_ -∗ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+  | |- _ ⊢ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+  end.
+
 (** * Specialize *)
 Record iTrm {X As} :=
   ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
@@ -303,36 +369,58 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
           let Q := match goal with |- IntoWand ?P ?Q _ => Q end in
           apply _ || fail "iSpecialize: cannot instantiate" P "with" Q
          |env_cbv; reflexivity|go H1 pats]
-    | SGoalPersistent :: ?pats =>
-       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
+    | SPureGoal ?d :: ?pats =>
+       eapply tac_specialize_assert_pure with _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |let Q := match goal with |- PersistentP ?Q => Q end in
-          apply _ || fail "iSpecialize:" Q "not persistent"
+         |let Q := match goal with |- FromPure ?Q _ => Q end in
+          apply _ || fail "iSpecialize:" Q "not pure"
          |env_cbv; reflexivity
-         |(*goal*)
+         |done_if d (*goal*)
          |go H1 pats]
-    | SGoalPure :: ?pats =>
-       eapply tac_specialize_assert_pure with _ H1 _ _ _ _ _;
+    | SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
+       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |let Q := match goal with |- FromPure ?Q _ => Q end in
-          apply _ || fail "iSpecialize:" Q "not pure"
+         |let Q := match goal with |- PersistentP ?Q => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
          |env_cbv; reflexivity
-         |(*goal*)
+         |iFrame Hs_frame; done_if d (*goal*)
          |go H1 pats]
-    | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs) :: ?pats =>
+    | SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
+       fail "iSpecialize: cannot select hypotheses for persistent premise"
+    | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
        let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
        eapply tac_specialize_assert with _ _ _ H1 _ lr Hs' _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |match m with
-          | false => apply elim_modal_dummy
-          | true => apply _ || fail "iSpecialize: goal not a modality"
+         |lazymatch m with
+          | GSpatial => apply elim_modal_dummy
+          | GModal => apply _ || fail "iSpecialize: goal not a modality"
           end
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
-         |iFrame Hs_frame (*goal*)
+         |iFrame Hs_frame; done_if d (*goal*)
          |go H1 pats]
+    | SAutoFrame GPersistent :: ?pats =>
+       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |let Q := match goal with |- PersistentP ?Q => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
+         |env_cbv; reflexivity
+         |solve [iFrame "∗ #"]
+         |go H1 pats]
+    | SAutoFrame ?m :: ?pats =>
+       eapply tac_specialize_frame with _ H1 _ _ _ _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |lazymatch m with
+          | GSpatial => apply elim_modal_dummy
+          | GModal => apply _ || fail "iSpecialize: goal not a modality"
+          end
+         |iFrame "∗ #"; apply tac_unlock
+           || fail "iSpecialize: premise cannot be solved by framing"
+         |reflexivity]; iIntro H1; go H1 pats
     end in let pats := spec_pat.parse pat in go H pats.
 
 (* The argument [p] denotes whether the conclusion of the specialized term is
@@ -740,71 +828,6 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
   iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 ) pat.
 
 (** * Introduction tactic *)
-Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
-  try iStartProof;
-  try first
-    [(* (∀ _, _) *) apply tac_forall_intro
-    |(* (?P → _) *) eapply tac_impl_intro_pure;
-      [let P := match goal with |- IntoPure ?P _ => P end in
-       apply _ || fail "iIntro:" P "not pure"|]
-    |(* (?P -∗ _) *) eapply tac_wand_intro_pure;
-      [let P := match goal with |- IntoPure ?P _ => P end in
-       apply _ || fail "iIntro:" P "not pure"|]
-    |(* ⌜∀ _, _⌝ *) apply tac_pure_forall_intro
-    |(* ⌜_ → _⌝ *) apply tac_pure_impl_intro];
-  intros x.
-
-Local Tactic Notation "iIntro" constr(H) :=
-  iStartProof;
-  first
-  [ (* (?Q → _) *)
-    eapply tac_impl_intro with _ H; (* (i:=H) *)
-      [reflexivity || fail 1 "iIntro: introducing" H
-                             "into non-empty spatial context"
-      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
-  | (* (_ -∗ _) *)
-    eapply tac_wand_intro with _ H; (* (i:=H) *)
-      [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
-  | fail 1 "iIntro: nothing to introduce" ].
-
-Local Tactic Notation "iIntro" "#" constr(H) :=
-  iStartProof;
-  first
-  [ (* (?P → _) *)
-    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
-      [let P := match goal with |- IntoPersistentP ?P _ => P end in
-       apply _ || fail 1 "iIntro: " P " not persistent"
-      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
-  | (* (?P -∗ _) *)
-    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
-      [let P := match goal with |- IntoPersistentP ?P _ => P end in
-       apply _ || fail 1 "iIntro: " P " not persistent"
-      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
-  | fail 1 "iIntro: nothing to introduce" ].
-
-Local Tactic Notation "iIntro" "_" :=
-  try iStartProof;
-  first
-  [ (* (?Q → _) *) apply tac_impl_intro_drop
-  | (* (_ -∗ _) *) apply tac_wand_intro_drop
-  | (* (∀ _, _) *) iIntro (_)
-  | fail 1 "iIntro: nothing to introduce" ].
-
-Local Tactic Notation "iIntroForall" :=
-  try iStartProof;
-  lazymatch goal with
-  | |- ∀ _, ?P => fail
-  | |- ∀ _, _ => intro
-  | |- _ ⊢ (∀ x : _, _) => let x' := fresh x in iIntro (x')
-  end.
-Local Tactic Notation "iIntro" :=
-  try iStartProof;
-  lazymatch goal with
-  | |- _ → ?P => intro
-  | |- _ ⊢ (_ -∗ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
-  | |- _ ⊢ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
-  end.
-
 Tactic Notation "iIntros" constr(pat) :=
   let rec go pats :=
     lazymatch pats with
@@ -824,6 +847,7 @@ Tactic Notation "iIntros" constr(pat) :=
     | ISimpl :: ?pats => simpl; go pats
     | IClear ?H :: ?pats => iClear H; go pats
     | IClearFrame ?H :: ?pats => iFrame H; go pats
+    | IDone :: ?pats => try done; go pats
     (* Introduction + destruct *)
     | IAlwaysElim ?pat :: ?pats =>
        let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
@@ -1245,40 +1269,50 @@ Tactic Notation "iAssertCore" open_constr(Q)
   let H := iFresh in
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with
-  | [SGoalPersistent] =>
+  | [SPureGoal ?d] =>
+     eapply tac_assert_pure with _ H Q _;
+       [env_cbv; reflexivity
+       |apply _ || fail "iAssert:" Q "not pure"
+       |done_if d (*goal*)
+       |tac H]
+  | [SGoal (SpecGoal GPersistent _ ?Hs_frame [] ?d)] =>
      eapply tac_assert_persistent with _ _ _ true [] H Q;
        [env_cbv; reflexivity
        |env_cbv; reflexivity
-       |(*goal*)
        |apply _ || fail "iAssert:" Q "not persistent"
+       |iFrame Hs_frame; done_if d (*goal*)
        |tac H]
-  | [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] =>
+  | [SGoal (SpecGoal GPersistent false ?Hs_frame _ ?d)] =>
+     fail "iAssert: cannot select hypotheses for persistent proposition"
+  | [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d)] =>
      let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
-     match eval cbv in (p && negb m) with
+     let p' := eval cbv in (match m with GModal => false | _ => p end) in
+     match p' with
      | false =>
        eapply tac_assert with _ _ _ lr Hs' H Q _;
-         [match m with
-          | false => apply elim_modal_dummy
-          | true => apply _ || fail "iAssert: goal not a modality"
+         [lazymatch m with
+          | GSpatial => apply elim_modal_dummy
+          | GModal => apply _ || fail "iAssert: goal not a modality"
           end
          |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
          |env_cbv; reflexivity
-         |iFrame Hs_frame (*goal*)
+         |iFrame Hs_frame; done_if d (*goal*)
          |tac H]
      | true =>
        eapply tac_assert_persistent with _ _ _ lr Hs' H Q;
          [env_cbv; reflexivity
          |env_cbv; reflexivity
-         |(*goal*)
          |apply _ || fail "iAssert:" Q "not persistent"
+         |done_if d (*goal*)
          |tac H]
      end
   | ?pat => fail "iAssert: invalid pattern" pat
   end.
+
 Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
   let p := intro_pat_persistent p in
   match p with
-  | true => iAssertCore Q with "[-]" as p tac
+  | true => iAssertCore Q with "[#]" as p tac
   | false => iAssertCore Q with "[]" as p tac
   end.
 
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
index be8d97c4e5a8496a3a1c0e3e90e1eaee166681b0..c48893cfcbba21bf036e23994c69e889730ba369 100644
--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
@@ -20,6 +20,7 @@ Inductive token :=
   | TAlwaysIntro : token
   | TModalIntro : token
   | TSimpl : token
+  | TDone : token
   | TForall : token
   | TAll : token
   | TMinus : token
@@ -46,6 +47,9 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_name kn k) ""
   | String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_name kn k) ""
   | String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_name kn k) ""
+  | String "/" (String "/" (String "=" s)) =>
+     tokenize_go s (TSimpl :: TDone :: cons_name kn k) ""
+  | String "/" (String "/" s) => tokenize_go s (TDone :: cons_name kn k) ""
   | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
   | String "*" (String "*" s) => tokenize_go s (TAll :: cons_name kn k) ""
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index f8c169ca0efcd66de0f7c113530c24db7bde75c5..c3a00b51cb7b0221698108c1ad5c200471c8b7f6 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -32,7 +32,7 @@ Proof.
   iIntros "{$Hac $Ha}".
   iExists (S j + z1), z2.
   iNext.
-  iApply ("H3" $! _ 0 with "H1 []").
+  iApply ("H3" $! _ 0 with "[$]").
   - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
   - done.
 Qed.
@@ -63,14 +63,14 @@ Definition foo {M} (P : uPred M) := (P → P)%I.
 Definition bar {M} : uPred M := (∀ P, foo P)%I.
 
 Lemma demo_4 (M : ucmraT) : True -∗ @bar M.
-Proof. iIntros. iIntros (P) "HP". done. Qed.
+Proof. iIntros. iIntros (P) "HP //". Qed.
 
 Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
   (∀ z, P → z ≡ y) -∗ (P -∗ (x,x) ≡ (y,x)).
 Proof.
   iIntros "H1 H2".
-  iRewrite (uPred.internal_eq_sym x x with "[#]"); first done.
-  iRewrite -("H1" $! _ with "[-]"); first done.
+  iRewrite (uPred.internal_eq_sym x x with "[# //]").
+  iRewrite -("H1" $! _ with "[- //]").
   done.
 Qed.
 
@@ -80,7 +80,7 @@ Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
 Proof.
   iIntros (a) "*".
   iIntros "#Hfoo **".
-  by iIntros "# _".
+  iIntros "# _ //".
 Qed.
 
 Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
@@ -96,10 +96,8 @@ Section iris.
     (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.
   Proof.
     iIntros (?) "H HP HQ".
-    iApply ("H" with "[#] HP >[HQ] >").
-    - done.
-    - by iApply inv_alloc.
-    - done.
+    iApply ("H" with "[% //] [$] [> HQ] [> //]").
+    by iApply inv_alloc.
   Qed.
 End iris.
 
@@ -119,14 +117,14 @@ Qed.
 
 Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
   (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
-Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.
+Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
 
 (* Check coercions *)
 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.