diff git a/ProofMode.md b/ProofMode.md
index 29dfbd9cf592b38621cf53102376d7d64362fefc..529ede69dfa410631ad69671539d513f903fa32f 100644
 a/ProofMode.md
+++ b/ProofMode.md
@@ 152,17 +152,19 @@ Rewriting / simplification
equality in the proof mode goal / hypothesis `H`.
 `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite in reverse direction
using an internal equality in the proof mode goal / hypothesis `H`.
 `iEval (tac)` / `iEval (tac) in H` : performs a tactic `tac` on the proof mode
 goal / hypothesis `H`. The tactic `tac` should be a reduction or rewriting
 tactic like `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
 tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar` where `P`
 is the proof goal / hypothesis `H`. After running `tac`, `?evar` is unified
 with the resulting `P`, which in turn becomes the new proof mode goal /
 hypothesis `H`.
 Note that parentheses around `tac` are needed.
 If `H` is a list of hypothesis, then `iEval` will perform `tac` on each of them.
 `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
 hypothesis `H`. This is a shorthand for `iEval (simpl)`.
+ `iEval (tac)` / `iEval (tac) in "selpat"` : performs a tactic `tac`
+ on the proof mode goal / hypotheses given by the selection pattern
+ `selpat`. Using `%` as part of the selection pattern is unsupported.
+ The tactic `tac` should be a reduction or rewriting tactic like
+ `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
+ tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar`
+ where `P` is the proof goal / a hypothesis given by `selpat`. After
+ running `tac`, `?evar` is unified with the resulting `P`, which in
+ turn becomes the new proof mode goal / a hypothesis given by
+ `selpat`. Note that parentheses around `tac` are needed.
+ `iSimpl` / `iSimpl in "selpat"` : performs `simpl` on the proof mode
+ goal / hypotheses given by the selection pattern `selpat`. This is a
+ shorthand for `iEval (simpl)`.
Iris
diff git a/tests/proofmode.ref b/tests/proofmode.ref
index 8dd4d71389a44d98c87363ad04ff85705e327ea0..1004ce814f670ae1be068f8443222080987cfc51 100644
 a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ 111,6 +111,17 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P ∗ False)%I wi
∗
⌜S (S (S x)) = y⌝
+1 subgoal
+
+ PROP : sbi
+ x, y, z : nat
+ ============================
+ "H1" : ⌜S (S (S x)) = y⌝
+ □
+ "H2" : ⌜(1 + y)%nat = z⌝
+ ∗
+ ⌜S (S (S x)) = y⌝
+
"test_iFrame_later_1"
: string
1 subgoal
diff git a/tests/proofmode.v b/tests/proofmode.v
index b8762b7aead1076ba0b88321736ed1eab919867a..528eec38e7d4444508db6c4c8424bc1436c876b1 100644
 a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ 478,6 +478,11 @@ Lemma test_iSimpl_in_2 x y z :
⌜ S (S (S x)) = y ⌝ : PROP.
Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed.
+Lemma test_iSimpl_in3 x y z :
+ ⌜ (3 + x)%nat = y ⌝ ∗ ⌜ (1 + y)%nat = z ⌝ ∗
+ ⌜ S (S (S x)) = y ⌝ : PROP.
+Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.
+
Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : PROP)%I.
Proof. by iIntros (?). Qed.
diff git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index b62920a2c466ff131e76c3ccb7a639eb5e7b6069..bb9c0726bf64326c21d1da29dc7b2984f41d470a 100644
 a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ 107,40 +107,6 @@ Ltac iFresh :=
constr:(IAnon n)
end.
(** * Simplification *)
Tactic Notation "iEval" tactic(t) :=
 iStartProof;
 eapply tac_eval;
 [let x := fresh in intros x; t; unfold x; reflexivity
 ].

Ltac iEval_go t Hs :=
 match Hs with
  [] => idtac
  ?H :: ?Hs =>
 let H := pretty_ident H in
 eapply tac_eval_in with _ H _ _ _;
 [pm_reflexivity  fail "iEval:" H "not found"
 let x := fresh in intros x; t; unfold x; reflexivity
 pm_reflexivity
 iEval_go t Hs]
 end.

Tactic Notation "iEval" tactic(t) "in" constr(H) :=
 iStartProof;
 let Hs := words H in iEval_go t Hs.

Tactic Notation "iSimpl" := iEval (simpl).
Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.

(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:

 https://sympa.inria.fr/sympa/arc/coqclub/201801/msg00000.html

PMP told me (= Robbert) in person that this is not possible with the current
Ltac, but it may be possible in Ltac2. *)

(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
@@ 151,9 +117,12 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
let H2 := pretty_ident H2 in
fail "iRename:" H2 "not fresh"].
+(** Elaborated selection patterns, unlike the type [sel_pat], contains
+only specific identifiers, and no wildcards like `#` (with the
+exception of the pure selection pattern `%`) *)
Inductive esel_pat :=
 ESelPure
  ESelIdent : bool → ident → esel_pat.
+  ESelIdent : (* whether the ident is intuitionistic *) bool → ident → esel_pat.
Local Ltac iElaborateSelPat_go pat Δ Hs :=
lazymatch pat with
@@ 175,6 +144,8 @@ Local Ltac iElaborateSelPat_go pat Δ Hs :=
fail "iElaborateSelPat:" H "not found"
end
end.
+(** Converts a selection pattern (given as a string) to a list of
+elaborated selection patterns. *)
Ltac iElaborateSelPat pat :=
lazymatch goal with
  envs_entails ?Δ _ =>
@@ 204,6 +175,39 @@ Tactic Notation "iClear" constr(Hs) :=
Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
iClear Hs; clear xs.
+(** ** Simplification *)
+Tactic Notation "iEval" tactic(t) :=
+ iStartProof;
+ eapply tac_eval;
+ [let x := fresh in intros x; t; unfold x; reflexivity
+ ].
+
+Local Ltac iEval_go t Hs :=
+ lazymatch Hs with
+  [] => idtac
+  ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
+  ESelIdent _ ?H :: ?Hs =>
+ eapply tac_eval_in with _ H _ _ _;
+ [pm_reflexivity  let H := pretty_ident H in fail "iEval:" H "not found"
+ let x := fresh in intros x; t; unfold x; reflexivity
+ pm_reflexivity
+ iEval_go t Hs]
+ end.
+
+Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
+ iStartProof; let Hs := iElaborateSelPat Hs in iEval_go t Hs.
+
+Tactic Notation "iSimpl" := iEval (simpl).
+Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.
+
+(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
+pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
+
+ https://sympa.inria.fr/sympa/arc/coqclub/201801/msg00000.html
+
+PMP told me (= Robbert) in person that this is not possible with the current
+Ltac, but it may be possible in Ltac2. *)
+
(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
eapply tac_assumption with _ H _ _; (* (i:=H) *)