diff --git a/ProofMode.md b/ProofMode.md
index 072c66c7252c4b34f90c354dee484d4fce8758de..a1507dfba484b0b006f12fb373b83a55a9b11c33 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.
 
@@ -238,7 +240,7 @@ _specification patterns_ to express splitting of hypotheses:
 - `[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.
+  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
   is a modality, in which case the modality will be kept in the generated goal
@@ -246,19 +248,29 @@ _specification patterns_ to express splitting of hypotheses:
 - `>[-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`
+- `[#]` : 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.
+  `P`, as well the remaining goal. The pattern can optionally contain 
+  hypotheses prefixed with a `$`, which results in them being framed in the
+  generated goal for the premise.
 - `[%]` : 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.
+- `[$]` :
+- `[# $]` :
+- `>[$]` :
+
+The specialization patterns `[H1 .. H2]`, `[-H1 ... Hn]`, `>[H1 ... Hn]`,
+`>[H1 ... Hn]`, `[#]` and `[%]` can optionally be ended with a `//`. This causes
+the `done` tactic being called to close the goal (after framing).
 
 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/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/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 2e5428ddc1d807cb7a247df4801be0fbf500565f..03b61878d0e033cffe79f1a491f352036f15c17c 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -131,9 +131,9 @@ Proof.
   destruct (to_val e) as [v|] eqn:?.
   { 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..92c215d55608589ed51b93399e16d570b052ff53 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,34 @@ 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)
+  | TModal :: TBracketL :: 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 :: 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
-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..13a85e4c5a0c113e5593dd3dc0e0ec6ee5b3ad69 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 "[% //] HP >[HQ] >[//]").
+    by iApply inv_alloc.
   Qed.
 End iris.
 
@@ -119,7 +117,7 @@ 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.