diff --git a/CHANGELOG.md b/CHANGELOG.md
index 62570bec7cd4034bf24a320bbc3c657d7053efa7..012580e53d83aad5402bfec4eae32bfda0527580 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,6 +46,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   basic proofmode support.
 * Sealed the definitions of `big_opS`, `big_opMS`, `big_opM` and `big_sepM2`
   to prevent undesired simplification.
+* Better handling of persistent results in `iDestruct`, `iPoseProof`, `iAssert`,
+  and friends. See https://gitlab.mpi-sws.org/iris/iris/merge_requests/341 for
+  more details.
 
 ## Iris 3.2.0 (released 2019-08-29)
 
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 6cbde74af585b88184beb7098640ccd525d82a3c..93b90699c55e66edf9d87d38478d714bf882be8d 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -66,6 +66,24 @@ In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
 "<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
 Tactic failure: iElaborateSelPat: "HQ" not found.
 The command has indeed failed with message:
+In nested Ltac calls to "iSpecialize (open_constr) as #",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) as (constr)" and
+"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
+last call failed.
+Tactic failure: iSpecialize: Q not persistent.
+"test_iAssert_intuitionistic"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first  done",
+"<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first  done",
+"iAssert (open_constr) with (constr) as (constr)",
+"iAssertCore (open_constr) with (constr) as (constr) (tactic3)",
+"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
+"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
+failed.
+Tactic failure: iSpecialize: (|==> P)%I not persistent.
+The command has indeed failed with message:
 In nested Ltac calls to "iSpecialize (open_constr)",
 "iSpecializeCore (open_constr) as (constr)",
 "iSpecializeCore (open_constr) as (constr)",
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9194db0b7f8de8952bbe7480443ee2ce87ea1923..27b0a34e1f1de36da34a5ae7c63d143e420d6cc8 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -157,6 +157,62 @@ Lemma test_iSpecialize_Coq_entailment P Q R :
   P → (P -∗ Q) → Q.
 Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
 
+Lemma test_iSpecialize_intuitionistic P Q R :
+  □ P -∗ □ (P -∗ P -∗ P -∗ P -∗ □ P -∗ P -∗ Q) -∗ R -∗ R ∗ □ (P ∗ Q).
+Proof.
+  iIntros "#HP #H HR".
+  (* Test that [H] remains in the intuitionistic context *)
+  iSpecialize ("H" with "HP").
+  iSpecialize ("H" with "[HP]"); first done.
+  iSpecialize ("H" with "[]"); first done.
+  iSpecialize ("H" with "[-HR]"); first done.
+  iSpecialize ("H" with "[#]"); first done.
+  iFrame "HR".
+  iSpecialize ("H" with "[-]"); first done.
+  by iFrame "#".
+Qed.
+
+Lemma test_iSpecialize_intuitionistic_2 P Q R :
+  □ P -∗ □ (P -∗ P -∗ P -∗ P -∗ □ P -∗ P -∗ Q) -∗ R -∗ R ∗ □ (P ∗ Q).
+Proof.
+  iIntros "#HP #H HR".
+  (* Test that [H] remains in the intuitionistic context *)
+  iSpecialize ("H" with "HP") as #.
+  iSpecialize ("H" with "[HP]") as #; first done.
+  iSpecialize ("H" with "[]") as #; first done.
+  iSpecialize ("H" with "[-HR]") as #; first done.
+  iSpecialize ("H" with "[#]") as #; first done.
+  iFrame "HR".
+  iSpecialize ("H" with "[-]") as #; first done.
+  by iFrame "#".
+Qed.
+
+Lemma test_iSpecialize_intuitionistic_3 P Q R :
+  P -∗ □ (P -∗ Q) -∗ □ (P -∗ <pers> Q) -∗ □ (Q -∗ R) -∗ P ∗ □ (Q ∗ R).
+Proof.
+  iIntros "HP #H1 #H2 #H3".
+  (* Should fail, [Q] is not persistent *)
+  Fail iSpecialize ("H1" with "HP") as #.
+  (* Should succeed, [<pers> Q] is persistent *)
+  iSpecialize ("H2" with "HP") as #.
+  (* Should succeed, despite [R] not being persistent, no spatial premises are
+  needed to prove [Q] *)
+  iSpecialize ("H3" with "H2") as #.
+  by iFrame "#".
+Qed.
+
+Check "test_iAssert_intuitionistic".
+Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
+  □ P -∗ □ |==> P.
+Proof.
+  iIntros "#HP".
+  (* Test that [HPupd1] ends up in the intuitionistic context *)
+  iAssert (|==> P)%I with "[]" as "#HPupd1"; first done.
+  (* This should not work, [|==> P] is not persistent. *)
+  Fail iAssert (|==> P)%I with "[#]" as "#HPupd2"; first done.
+  done.
+Qed.
+
 Lemma test_iPure_intro_emp R `{!Affine R} :
   R -∗ emp.
 Proof. iIntros "HR". by iPureIntro. Qed.
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index c28fbbe9d5bd6833e200a93dd95f6dba478b9bd7..e50c8c88d01afe04a894150f55358621b3b51f45 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -17,6 +17,10 @@ the actual operations that may appear in users' proofs. *)
 Lemma lazy_andb_true (b1 b2 : bool) : b1 &&& b2 = true ↔ b1 = true ∧ b2 = true.
 Proof. destruct b1, b2; intuition congruence. Qed.
 
+Definition negb (b : bool) : bool := if b then false else true.
+Lemma negb_true b : negb b = true ↔ b = false.
+Proof. by destruct b. Qed.
+
 Fixpoint Pos_succ (x : positive) : positive :=
   match x with
   | (p~1)%positive => ((Pos_succ p)~0)%positive
@@ -94,7 +98,10 @@ Qed.
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
 
-(** Copies of some [option] combinators for better reduction control. *)
+(** Copies of some functions on [list] and [option] for better reduction control. *)
+Fixpoint pm_app {A} (l1 l2 : list A) : list A :=
+  match l1 with [] => l2 | x :: l1 => x :: pm_app l1 l2 end.
+
 Definition pm_option_bind {A B} (f : A → option B) (mx : option A) : option B :=
   match mx with Some x => f x | None => None end.
 Arguments pm_option_bind {_ _} _ !_ /.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 757a3b6c610ef7c6048342136e221a05233f66aa..50d3c69880b399ca0a05a319564bac9bcd051ef5 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -286,13 +286,14 @@ Proof.
   - by rewrite HR assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert Δ j q neg js R P1 P2 P1' Q :
+Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
   envs_lookup j Δ = Some (q, R) →
-  IntoWand q false R P1 P2 → AddModal P1' P1 Q →
+  IntoWand q false R P1 P2 →
+  (if am then AddModal P1' P1 Q else TCEq P1' P1) →
   match
     ''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left)
-    js (envs_delete true j q Δ);
-    Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
+                           js (envs_delete true j q Δ);
+    Δ2' ← envs_app (negb am &&& q &&& env_spatial_is_nil Δ1) (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2') (* does not preserve position of [j] *)
   with
   | Some (Δ1,Δ2') =>
@@ -301,15 +302,21 @@ Lemma tac_specialize_assert Δ j q neg js R P1 P2 P1' Q :
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros ??? HQ.
+  rewrite envs_entails_eq. intros ?? Hmod HQ.
   destruct (_ ≫= _) as [[Δ1 Δ2']|] eqn:?; last done.
   destruct HQ as [HP1 HQ].
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_singleton_sound Δ2) //; simpl.
-  rewrite HP1 (into_wand q false) /= -(add_modal P1' P1 Q). cancel [P1'].
-  apply wand_intro_l. by rewrite assoc !wand_elim_r.
+  rewrite -intuitionistically_if_idemp (into_wand q false) /=.
+  destruct (negb am &&& q &&& env_spatial_is_nil Δ1) eqn:Hp; simpl.
+  - move: Hp. rewrite !lazy_andb_true negb_true. intros [[-> ->] ?]; simpl.
+    destruct Hmod. rewrite env_spatial_is_nil_intuitionistically // HP1.
+    by rewrite assoc intuitionistically_sep_2 wand_elim_l wand_elim_r HQ.
+  - rewrite intuitionistically_if_elim HP1. destruct am; last destruct Hmod.
+    + by rewrite assoc -(comm _ P1') -assoc wand_trans HQ.
+    + by rewrite assoc wand_elim_l wand_elim_r HQ.
 Qed.
 
 Lemma tac_unlock_emp Δ Q : envs_entails Δ Q → envs_entails Δ (emp ∗ locked Q).
@@ -319,18 +326,18 @@ Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
 Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
 Proof. by unlock. Qed.
 
-Lemma tac_specialize_frame Δ j q R P1 P2 P1' Q Q' :
+Lemma tac_specialize_frame Δ j (q am : bool) R P1 P2 P1' Q Q' :
   envs_lookup j Δ = Some (q, R) →
   IntoWand q false R P1 P2 →
-  AddModal P1' P1 Q →
+  (if am then AddModal P1' P1 Q else TCEq P1' P1) →
   envs_entails (envs_delete true j q Δ) (P1' ∗ locked Q') →
   Q' = (P2 -∗ Q)%I →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros ??? HPQ ->.
+  rewrite envs_entails_eq. intros ?? Hmod HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
-  rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
-  apply wand_intro_l. by rewrite assoc !wand_elim_r.
+  rewrite (into_wand q false) /= assoc -(comm _ P1') -assoc wand_trans.
+  destruct am; [done|destruct Hmod]. by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index d9ff74e69a6f454e0a87c4318b7a4f7fd9857d3e..5fdeb14cc77258d73d0913264daf06ef0db9f441 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -903,15 +903,13 @@ Ltac iSpecializePat_go H1 pats :=
        fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
     | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
        let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
-       notypeclasses refine (tac_specialize_assert _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_assert _ H1 _
+           (if m is GModal then true else false) lr Hs' _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |lazymatch m with
-          | GSpatial => class_apply add_modal_id
-          | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
-          end
+         |iSolveTC || fail "iSpecialize: goal not a modality"
          |pm_reduce;
           lazymatch goal with
           | |- False =>
@@ -934,15 +932,13 @@ Ltac iSpecializePat_go H1 pats :=
          |pm_reduce; solve [iFrame "∗ #"]
          |pm_reduce; iSpecializePat_go H1 pats]
     | SAutoFrame ?m :: ?pats =>
-       notypeclasses refine (tac_specialize_frame _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_frame _ H1 _
+           (if m is GModal then true else false) _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |lazymatch m with
-          | GSpatial => class_apply add_modal_id
-          | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
-          end
+         |iSolveTC || fail "iSpecialize: goal not a modality"
          |pm_reduce;
           first
             [notypeclasses refine (tac_unlock_emp _ _ _)
@@ -955,15 +951,66 @@ Ltac iSpecializePat_go H1 pats :=
 Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
   let pats := spec_pat.parse pat in iSpecializePat_go H pats.
 
-(** The argument [p] denotes whether the conclusion of the specialized term is
-intuitionistic. If so, one can use all spatial hypotheses for both proving the
-premises and the remaning goal. The argument [p] can either be a Boolean or an
-introduction pattern, which will be coerced into [true] when it solely contains
-`#` or `%` patterns at the top-level.
+(** The tactics [iSpecialize trm as #] and [iSpecializeCore trm as true] allow
+one to use the entire spatial context /twice/: the first time for proving the
+premises [Q1 .. Qn] of [H : Q1 -* .. -∗ Qn -∗ R], and the second time for
+proving the remaining goal. This is possible if all of the following properties
+hold:
+1. The conclusion [R] of the hypothesis [H] is persistent.
+2. The specialization pattern [[> ..]] for wrapping a modality is not used for
+   any of the premises [Q1 .. Qn].
+3. The BI is either affine, or the hypothesis [H] resides in the intuitionistic
+   context.
+
+The copying of the context for proving the premises of [H] and the remaining
+goal is implemented using the lemma [tac_specialize_intuitionistic_helper].
+
+Since the tactic [iSpecialize .. as #] is used a helper to implement
+[iDestruct .. as "#.."], [iPoseProof .. as "#.."], [iSpecialize .. as "#.."],
+and friends, the behavior on violations of these conditions is as follows:
+
+- If condition 1 is violated (i.e. the conclusion [R] of [H] is not persistent),
+  the tactic will fail.
+- If condition 2 or 3 is violated, the tactic will fall back to consuming the
+  hypotheses for proving the premises [Q1 .. Qn]. That is, it will fall back to
+  not using [tac_specialize_intuitionistic_helper].
+
+The function [use_tac_specialize_intuitionistic_helper Δ pat] below returns
+[true] iff the specialization pattern [pat] consumes any spatial hypotheses,
+and does not contain the pattern [[> ..]] (cf. condition 2). If the function
+returns [false], then the conclusion can be moved in the intuitionistic context
+even if conditions 1 and 3 do not hold. Therefore, in that case, we prefer
+putting the conclusion to the intuitionistic context directly and not using
+[tac_specialize_intuitionistic_helper], which requires conditions 1 and 3. *)
+Fixpoint use_tac_specialize_intuitionistic_helper {M}
+    (Δ : envs M) (pats : list spec_pat) : bool :=
+  match pats with
+  | [] => false
+  | (SForall | SPureGoal _) :: pats =>
+     use_tac_specialize_intuitionistic_helper Δ pats
+  | SAutoFrame _ :: _ => true
+  | SIdent H _ :: pats =>
+     match envs_lookup_delete false H Δ with
+     | Some (false, _, Δ) => true
+     | Some (true, _, Δ) => use_tac_specialize_intuitionistic_helper Δ pats
+     | None => false (* dummy case (invalid pattern, will fail in the tactic anyway) *)
+     end
+  | SGoal (SpecGoal GModal _ _ _ _) :: _ => false
+  | SGoal (SpecGoal GIntuitionistic _ _ _ _) :: pats =>
+     use_tac_specialize_intuitionistic_helper Δ pats
+  | SGoal (SpecGoal GSpatial neg Hs_frame Hs _) :: pats =>
+     match envs_split (if neg is true then Right else Left)
+                      (if neg then Hs else pm_app Hs_frame Hs) Δ with
+     | Some (Δ1,Δ2) => if env_spatial_is_nil Δ1
+                       then use_tac_specialize_intuitionistic_helper Δ2 pats
+                       else true
+     | None => false (* dummy case (invalid pattern, will fail in the tactic anyway) *)
+     end
+  end.
 
-In case the specialization pattern in [t] states that the modality of the goal
-should be kept for one of the premises (i.e. [>[H1 .. Hn]] is used) then [p]
-defaults to [false] (i.e. spatial hypotheses are not preserved). *)
+(** The argument [p] of [iSpecializeCore] can either be a Boolean, or an
+introduction pattern that is coerced into [true] when it solely contains [#] or
+[%] patterns at the top-level. *)
 Tactic Notation "iSpecializeCore" open_constr(H)
     "with" open_constr(xs) open_constr(pat) "as" constr(p) :=
   let p := intro_pat_intuitionistic p in
@@ -976,25 +1023,17 @@ Tactic Notation "iSpecializeCore" open_constr(H)
   iSpecializeArgs H xs; [..|
     lazymatch type of H with
     | ident =>
-       (* The lemma [tac_specialize_intuitionistic_helper] allows one to use the
-       whole spatial context for:
-       - proving the premises of the lemma we specialize, and,
-       - the remaining goal.
-
-       We can only use if all of the following properties hold:
-       - The result of the specialization is persistent.
-       - No modality is eliminated.
-       - If the BI is not affine, the hypothesis should be in the intuitionistic
-         context.
-
-       As an optimization, we do only use [tac_specialize_intuitionistic_helper]
-       if no implications nor wands are eliminated, i.e. [pat ≠ []]. *)
        let pat := spec_pat.parse pat in
-       lazymatch eval compute in
-         (p && bool_decide (pat ≠ []) && negb (existsb spec_pat_modal pat)) with
+       let Δ := iGetCtx in
+       (* Check if we should use [tac_specialize_intuitionistic_helper]. Notice
+       that [pm_eval] does not unfold [use_tac_specialize_intuitionistic_helper],
+       so we should do that first. *)
+       let b := eval cbv [use_tac_specialize_intuitionistic_helper] in
+         (if p then use_tac_specialize_intuitionistic_helper Δ pat else false) in
+       lazymatch eval pm_eval in b with
        | true =>
-          (* Check that if the BI is not affine, the hypothesis is in the
-          intuitionistic context. *)
+          (* Check that the BI is either affine, or the hypothesis [H] resides
+          in the intuitionistic context. *)
           lazymatch iTypeOf H with
           | Some (?q, _) =>
              let PROP := iBiOfGoal in
@@ -1003,10 +1042,11 @@ Tactic Notation "iSpecializeCore" open_constr(H)
                 notypeclasses refine (tac_specialize_intuitionistic_helper _ H _ _ _ _ _ _ _ _ _ _);
                   [pm_reflexivity
                    (* This premise, [envs_lookup j Δ = Some (q,P)],
-                   holds because [iTypeOf] succeeded *)
+                   holds because the [iTypeOf] above succeeded *)
                   |pm_reduce; iSolveTC
-                   (* This premise, [if q then TCTrue else BiAffine PROP],
-                   holds because [q || TC_to_bool (BiAffine PROP)] is true *)
+                   (* This premise, [if q then TCTrue else BiAffine PROP], holds
+                   because we established that [q || TC_to_bool (BiAffine PROP)]
+                   is true *)
                   |iSpecializePat H pat;
                     [..
                     |notypeclasses refine (tac_specialize_intuitionistic_helper_done _ H _ _ _);
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index ba3090367327c75f7473f4cf1c7c2a96522ea36c..6ce3ffd9c6f798cb1d1daad4be072d3afa1fb945 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -6,7 +6,8 @@ From iris.proofmode Require Import base environments.
     do not reduce e.g. before unification happens in [iApply].*)
 Declare Reduction pm_eval := cbv [
   (* base *)
-  base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
+  base.negb base.beq
+  base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
   (* environments *)
   env_lookup env_lookup_delete env_delete env_app env_replace
   env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
@@ -15,8 +16,8 @@ Declare Reduction pm_eval := cbv [
   envs_clear_spatial envs_clear_intuitionistic envs_incr_counter
   envs_split_go envs_split
   env_to_prop_go env_to_prop env_to_prop_and_go env_to_prop_and
-  (* PM option combinators *)
-  pm_option_bind pm_from_option pm_option_fun
+  (* PM list and option functions *)
+  pm_app pm_option_bind pm_from_option pm_option_fun
 ].
 Ltac pm_eval t :=
   eval pm_eval in t.