diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index e3cdb5f5f135a13e3e3a7bf612a51c3eb54d700a..d09d019eae03506411f41af240a3e70d640c6a14 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -162,8 +162,7 @@ Qed.
 Lemma fupd_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
   (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={E1,E2}=∗ P) → ⊢ P.
 Proof.
-  iIntros (Hfupd).
-  apply later_soundness, bupd_soundness; [by apply later_plain|].
+  intros Hfupd. apply later_soundness, bupd_soundness; [by apply later_plain|].
   iMod fupd_soundness_no_lc_unfold as (hws ω) "(Hlc & Hω & #H)".
   iMod ("H" with "[Hlc] Hω") as "H'".
   { iMod (Hfupd with "Hlc") as "H'". iModIntro. iApply "H'". }
@@ -173,7 +172,7 @@ Qed.
 Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
   (∀ `{Hinv: !invGS_gen HasLc Σ}, £ n ={E1,E2}=∗ P) → ⊢ P.
 Proof.
-  iIntros (Hfupd). eapply (lc_soundness (S n)); first done.
+  intros Hfupd. eapply (lc_soundness (S n)); first done.
   intros Hc. rewrite lc_succ.
   iIntros "[Hone Hn]". rewrite -le_upd_trans. iApply bupd_le_upd.
   iMod wsat_alloc as (Hw) "[Hw HE]".
@@ -220,7 +219,7 @@ Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m
   (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={⊤}[∅]▷=∗^n P) →
   ⊢ P.
 Proof.
-  iIntros (Hiter). eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv.
+  intros Hiter. eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv.
   iIntros "Hcred". destruct n as [|n].
   { by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
    simpl in Hiter |- *. iMod (Hiter with "Hcred") as "H". iIntros "!>!>!>".
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 41172bf19414cc864fc4de173a272b8ad2f43c80..16d66473e3de0ce772ed5d67827fd3da712894b6 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -174,7 +174,7 @@ Local Lemma wp_progress_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} es σ1 n κs t2
   e2 ∈ t2 →
   not_stuck e2 σ2.
 Proof.
-  iIntros (Hwp ??).
+  intros Hwp ??.
   eapply pure_soundness.
   eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
@@ -232,7 +232,7 @@ Lemma wp_strong_adequacy_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} s es σ1 n κs
   (* Then we can conclude [φ] at the meta-level. *)
   φ.
 Proof.
-  iIntros (Hwp ?).
+  intros Hwp ?.
   eapply pure_soundness.
   eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index c5078fd677f6760dbdae83dd7adee3a64ed810d4..5bcd190ea6c99910b48cbc3b34eb160f1b637231 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -177,7 +177,7 @@ Lemma wp_pure_step_later `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
   ▷^n (£ n -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
-  enough (∀ P, ▷^n P ⊢ |={E}▷=>^n P) as Hwp by apply Hwp. iIntros (?).
+  enough (∀ P, ▷^n P ⊢ |={E}▷=>^n P) as Hwp by apply Hwp. intros ?.
   induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
 Qed.
 End lifting.
diff --git a/iris/proofmode/base.v b/iris/proofmode/base.v
index f782aeb3e8ea95f997bcf3e0d18050f94f32c474..80dfe224a68ef8454ec7e7eaaf805bd9b5bdbd5f 100644
--- a/iris/proofmode/base.v
+++ b/iris/proofmode/base.v
@@ -2,9 +2,27 @@ From Coq Require Export Ascii.
 From stdpp Require Export strings.
 From iris.prelude Require Export prelude.
 From iris.prelude Require Import options.
+From Ltac2 Require Ltac2.
 
 (** * Utility definitions used by the proofmode *)
 
+Ltac2 of_ltac1_list l := Option.get (Ltac1.to_list l).
+
+Ltac ltac1_list_iter tac l :=
+  let go := ltac2:(tac l |- List.iter (ltac1:(tac x |- tac x) tac)
+                                      (of_ltac1_list l)) in
+  go tac l.
+
+Ltac ltac1_list_rev_iter tac l :=
+  let go := ltac2:(tac l |- List.iter (ltac1:(tac x |- tac x) tac)
+                                      (List.rev (of_ltac1_list l))) in
+  go tac l.
+
+(* Sample use:
+Tactic Notation "foo" ident_list(xs) :=
+  ltac1_list_rev_iter ltac:(fun x => intros x) xs.
+*)
+
 (* Directions of rewrites *)
 Inductive direction := Left | Right.
 
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index d9289382bd972a190295a1c56b3a1726aeb12dbe..c96710a0dbf86e19a08cc4e0707eb1f378bb8822 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -390,10 +390,6 @@ Ltac iFramePure t :=
     [tc_solve || fail "iFrame: cannot frame" φ
     |iFrameFinish].
 
-Ltac2 with_ltac1_list f ls :=
-  let ls := Option.get (Ltac1.to_list ls) in
-  f ls.
-
 Ltac iFrameHyp H :=
   iStartProof;
   eapply tac_frame with H _ _ _;
@@ -426,14 +422,6 @@ Ltac iFrameAnySpatial :=
      let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
   end.
 
-Ltac2 iFramePures ts :=
-  with_ltac1_list (List.iter (ltac1:(t |- iFramePure t))) ts.
-
-Tactic Notation "iFrame" := iFrameAnySpatial.
-
-Tactic Notation "iFrame" "(" ne_constr_list(ts) ")" :=
-  let f := ltac2:(ts |- iFramePures ts) in f ts.
-
 Local Ltac iFrame_go Hs :=
   lazymatch Hs with
   | [] => idtac
@@ -443,14 +431,20 @@ Local Ltac iFrame_go Hs :=
   | SelIdent ?H :: ?Hs => iFrameHyp H; iFrame_go Hs
   end.
 
-Tactic Notation "iFrame" constr(Hs) :=
-  let Hs := sel_pat.parse Hs in iFrame_go Hs.
-Tactic Notation "iFrame" "(" ne_constr_list(ts) ")" constr(Hs) :=
-  let f := ltac2:(ts |- iFramePures ts) in f ts;
-  iFrame Hs.
+Ltac iFrame0_ Hs :=
+  let Hs := sel_pat.parse Hs in
+  iFrame_go Hs.
+Ltac iFrame_ ts Hs :=
+  ltac1_list_iter iFramePure ts;
+  iFrame0_ Hs.
+
+Tactic Notation "iFrame" := iFrameAnySpatial.
+Tactic Notation "iFrame" "(" ne_constr_list(ts) ")" := iFrame_ ts "".
+Tactic Notation "iFrame" constr(Hs) := iFrame0_ Hs.
+Tactic Notation "iFrame" "(" ne_constr_list(ts) ")" constr(Hs) := iFrame_ ts Hs.
 
 Tactic Notation "iFrame" "select" open_constr(pat) :=
-  iSelect pat ltac:(fun H => iFrame H).
+  iSelect pat ltac:(fun H => iFrameHyp H).
 
 (** * Basic introduction tactics *)
 Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
@@ -596,7 +590,7 @@ Local Tactic Notation "iIntro" :=
   end.
 
 (** * Revert *)
-Local Tactic Notation "iForallRevert" ident(x) :=
+Ltac iForallRevert x :=
   let err x :=
     intros x;
     iMatchHyp (fun H P =>
@@ -641,34 +635,29 @@ Tactic Notation "iRevertHyp" constr(H) "with" tactic1(tac) :=
 
 Tactic Notation "iRevertHyp" constr(H) := iRevertHyp H with (fun _ => idtac).
 
-Tactic Notation "iRevert" constr(Hs) :=
-  let rec go Hs :=
-    lazymatch Hs with
-    | [] => idtac
-    | ESelPure :: ?Hs =>
-       repeat match goal with x : _ |- _ => revert x end;
-       go Hs
-    | ESelIdent _ ?H :: ?Hs => iRevertHyp H; go Hs
-    end in
+Ltac iRevert_go Hs :=
+  lazymatch Hs with
+  | [] => idtac
+  | ESelPure :: ?Hs =>
+     repeat match goal with x : _ |- _ => revert x end;
+     iRevert_go Hs
+  | ESelIdent _ ?H :: ?Hs => iRevertHyp H; iRevert_go Hs
+  end.
+
+Ltac iRevert0_ Hs :=
   iStartProof;
   let Hs := iElaborateSelPat Hs in
-  (* No need to reverse [Hs], [iElaborateSelPat] already does that. *)
-  go Hs.
-
-Ltac2 iForallReverts ts :=
-  with_ltac1_list
-    (fun ts => List.iter (ltac1:(t |- iForallRevert t)) (List.rev ts))
-    ts.
+  iRevert_go Hs.
+Ltac iRevert_ xs Hs :=
+  iRevert0_ Hs;
+  ltac1_list_rev_iter iForallRevert xs.
 
-Tactic Notation "iRevert" "(" ne_ident_list(xs) ")" :=
-  let f := ltac2:(xs |- iForallReverts xs) in f xs.
-
-Tactic Notation "iRevert" "(" ne_ident_list(xs) ")" constr(Hs) :=
-  iRevert Hs;
-  let f := ltac2:(xs |- iForallReverts xs) in f xs.
+Tactic Notation "iRevert" constr(Hs) := iRevert0_ Hs.
+Tactic Notation "iRevert" "(" ne_ident_list(xs) ")" := iRevert_ xs "".
+Tactic Notation "iRevert" "(" ne_ident_list(xs) ")" constr(Hs) := iRevert_ xs Hs.
 
 Tactic Notation "iRevert" "select" open_constr(pat) :=
-  iSelect pat ltac:(fun H => iRevert H).
+  iSelect pat ltac:(fun H => iRevertHyp H).
 
 (** * The specialize and pose proof tactics *)
 Record iTrm {X As S} :=
@@ -1268,20 +1257,17 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :
 
 (** * Existential *)
 
-Ltac iExists_ x1 :=
+Ltac iExists_ x :=
   iStartProof;
   eapply tac_exist;
     [tc_solve ||
      let P := match goal with |- FromExist ?P _ => P end in
      fail "iExists:" P "not an existential"
-    |pm_prettify; eexists x1
+    |pm_prettify; eexists x
      (* subgoal *) ].
 
-Ltac2 iExistss xs :=
-  with_ltac1_list (List.iter ltac1:(x1 |- iExists_ x1)) xs.
-
 Tactic Notation "iExists" ne_uconstr_list_sep(xs,",") :=
-  let f := ltac2:(xs |- iExistss xs) in f xs.
+  ltac1_list_iter iExists_ xs.
 
 Local Tactic Notation "iExistDestruct" constr(H)
     "as" simple_intropattern(x) constr(Hx) :=
@@ -1471,33 +1457,18 @@ Local Ltac iDestructHypFindPat Hgo pat found pats :=
      | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
      end
   end.
-Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
+
+Ltac iDestructHyp0_ H pat :=
   let pats := intro_pat.parse pat in
   iDestructHypFindPat H pat false pats.
-
-Ltac2 iExistDestructs h xs :=
-  with_ltac1_list (List.iter (ltac1:(H x |- iExistDestruct H as x H) h)) xs.
-
 Ltac iDestructHyp_ H xs pat :=
-  let f := ltac2:(h xs |- iExistDestructs h xs) in f H xs;
-  iDestructHyp H as @ pat.
-
-Ltac iDestructHyp_intros_hd_ H xs pat :=
-  let f :=
-    ltac2:(h xs |-
-      with_ltac1_list
-        (fun xs =>
-           ltac1:(x1 |- intros x1) (List.hd xs);
-           List.iter (ltac1:(H x |- iExistDestruct H as x H) h) (List.tl xs)
-        )
-        xs
-    ) in
-  f H xs;
-  iDestructHyp H as @ pat.
-
-Tactic Notation "iDestructHyp" constr(H) "as" "(" ne_simple_intropattern_list(xs) ")"
-    constr(pat) :=
-  iDestructHyp_ H xs pat.
+  ltac1_list_iter ltac:(fun x => iExistDestruct H as x H) xs;
+  iDestructHyp0_ H pat.
+
+Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
+  iDestructHyp0_ H pat.
+Tactic Notation "iDestructHyp" constr(H) "as"
+  "(" ne_simple_intropattern_list(xs) ")" constr(pat) := iDestructHyp_ H xs pat.
 
 (** * Combinining hypotheses *)
 Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
@@ -1622,54 +1593,49 @@ Ltac iIntros_go pats startproof :=
   | ?pat :: ?pats =>
      let H := iFresh in iIntro H; iDestructHyp H as pat; iIntros_go pats false
   end.
-Tactic Notation "iIntros" constr(pat) :=
-  let pats := intro_pat.parse pat in iIntros_go pats true.
-Tactic Notation "iIntros" := iIntros [IAll].
 
-Ltac2 iIntross xs :=
-  with_ltac1_list (List.iter ltac1:(x |- iIntro (x))) xs.
-Ltac iIntros_ xs :=
-  let f := ltac2:(xs |- iIntross xs) in f xs.
+Ltac iIntros0_ pat :=
+  let pats := intro_pat.parse pat in
+  iIntros_go pats true.
+Ltac iIntros_ xs pat :=
+  ltac1_list_iter ltac:(fun x => iIntro (x)) xs;
+  iIntros0_ pat.
 
+Tactic Notation "iIntros" := iIntros0_ [IAll].
+Tactic Notation "iIntros" constr(pat) := iIntros0_ pat.
 Tactic Notation "iIntros" "(" ne_simple_intropattern_list(xs) ")" :=
-  iIntros_ xs.
-
-Tactic Notation "iIntros" "(" ne_simple_intropattern_list(xs) ")" constr(p) :=
-  iIntros_ xs;
-  iIntros p.
-
-Tactic Notation "iIntros" constr(p) "(" ne_simple_intropattern_list(xs) ")" :=
-  iIntros p;
-  iIntros_ xs.
-
-Tactic Notation "iIntros" constr(p1) "(" ne_simple_intropattern_list(xs) ")" constr(p2) :=
-  iIntros p1;
-  iIntros_ xs;
-  iIntros p2.
-
-(* Used for generalization in iInduction and iLöb *)
+  iIntros_ xs "".
+Tactic Notation "iIntros" "(" ne_simple_intropattern_list(xs) ")" constr(pat) :=
+  iIntros_ xs pat.
+Tactic Notation "iIntros" constr(pat) "(" ne_simple_intropattern_list(xs) ")" :=
+  iIntros0_ pat; iIntros_ xs "".
+Tactic Notation "iIntros" constr(pat1)
+    "(" ne_simple_intropattern_list(xs) ")" constr(pat2) :=
+  iIntros0_ pat1; iIntros_ xs pat2.
+
+(* Used for generalization in [iInduction] and [iLöb] *)
 Ltac iRevertIntros_go Hs tac :=
   lazymatch Hs with
-  | [] => tac
+  | [] => tac ()
   | ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
   | ESelIdent ?p ?H :: ?Hs => iRevertHyp H; iRevertIntros_go Hs tac; iIntro H as p
   end.
 
-Tactic Notation "iRevertIntros" constr(Hs) "with" tactic3(tac) :=
-  try iStartProof; let Hs := iElaborateSelPat Hs in iRevertIntros_go Hs tac.
-
-Ltac iRevertIntros_ Hs xs tac :=
-  let f := ltac2:(xs |- iForallReverts xs) in
-  iRevertIntros Hs with (f xs; tac; iIntros_ xs).
+Ltac iRevertIntros0_ Hs tac :=
+  try iStartProof;
+  let Hs := iElaborateSelPat Hs in
+  iRevertIntros_go Hs tac.
+Ltac iRevertIntros_ xs Hs tac :=
+  iRevertIntros0_ Hs ltac:(fun _ => iRevert_ xs ""; tac (); iIntros_ xs "").
 
+Tactic Notation "iRevertIntros" constr(Hs) "with" tactic3(tac) :=
+  iRevertIntros0_ Hs tac.
 Tactic Notation "iRevertIntros" "(" ne_ident_list(xs) ")" constr(Hs) "with" tactic3(tac):=
-  iRevertIntros_ Hs xs tac.
-
+  iRevertIntros_ xs Hs tac.
 Tactic Notation "iRevertIntros" "with" tactic3(tac) :=
-  iRevertIntros "" with tac.
+  iRevertIntros0_ "" tac.  
 Tactic Notation "iRevertIntros" "(" ne_ident_list(xs) ")" "with" tactic3(tac):=
-  let f := ltac2:(xs |- iForallReverts xs) in
-  iRevertIntros "" with (f xs; tac; iIntros (x1)).
+  iRevertIntros_ xs "" tac.
 
 (** * Destruct and PoseProof tactics *)
 (** The tactics [iDestruct] and [iPoseProof] are similar, but there are some
@@ -1778,7 +1744,8 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
          rev_tac j)
     | _ => rev_tac 0%N
     end in
-  tac; fix_ihs ltac:(fun _ => idtac).
+  tac ();
+  fix_ihs ltac:(fun _ => idtac).
 
 Ltac iHypsContaining x :=
   let rec go Γ x Hs :=
@@ -1794,45 +1761,53 @@ Ltac iHypsContaining x :=
   let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs _) _ => Γs end in
   let Hs := go Γp x (@nil ident) in go Γs x Hs.
 
-Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic3(tac) :=
-  iRevertIntros Hs with (
-    iRevertIntros "∗" with (
-      idtac;
+Ltac iInduction0_ x Hs tac IH :=
+  iRevertIntros0_ Hs ltac:(fun _ =>
+    iRevertIntros0_ "∗" ltac:(fun _ =>
       let Hsx := iHypsContaining x in
-      iRevertIntros Hsx with tac
+      iRevertIntros0_ Hsx ltac:(fun _ =>
+        iInductionCore tac as IH
+      )
+    )
+  ).
+Ltac iInduction_ x xs Hs tac IH :=
+  iRevertIntros0_ Hs ltac:(fun _ =>
+    iRevertIntros_ xs "∗" ltac:(fun _ =>
+      let Hsx := iHypsContaining x in
+      iRevertIntros0_ Hsx ltac:(fun _ =>
+        iInductionCore tac as IH
+      )
     )
   ).
 
+(* Without induction scheme *)
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) :=
-  iInductionRevert x "" with (iInductionCore (induction x as pat) as IH).
+  iInduction0_ x "" ltac:(fun _ => induction x as pat) IH.
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "forall" "(" ne_ident_list(xs) ")" :=
-  iInductionRevert x "" with (
-    iRevertIntros_ "" xs ltac:(idtac; iInductionCore (induction x as pat) as IH)).
+  iInduction_ x xs "" ltac:(fun _ => induction x as pat) IH.
 
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "forall" constr(Hs) :=
-  iInductionRevert x Hs with (iInductionCore (induction x as pat) as IH).
+  iInduction0_ x Hs ltac:(fun _ => induction x as pat) IH.
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "forall" "(" ne_ident_list(xs) ")" constr(Hs) :=
-  iInductionRevert x Hs with
-    (iRevertIntros_ "" xs ltac:(idtac; iInductionCore (induction x as pat) as IH)).
+  iInduction_ x xs Hs ltac:(fun _ => induction x as pat) IH.
 
+(* With induction scheme *)
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) :=
-  iInductionRevert x "" with (iInductionCore (induction x as pat using u) as IH).
+  iInduction0_ x "" ltac:(fun _ => induction x as pat using u) IH.
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) "forall" "(" ne_ident_list(xs) ")" :=
-  iInductionRevert x "" with (
-    iRevertIntros_ "" xs ltac:(idtac; iInductionCore (induction x as pat using u) as IH)).
+  iInduction_ x xs "" ltac:(fun _ => induction x as pat using u) IH.
 
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) "forall" constr(Hs) :=
-  iInductionRevert x Hs with (iInductionCore (induction x as pat using u) as IH).
+  iInduction0_ x Hs ltac:(fun _ => induction x as pat using u) IH.
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) "forall" "(" ne_ident_list(xs) ")" constr(Hs) :=
-  iInductionRevert x Hs with
-    (iRevertIntros_ "" xs ltac:(idtac; iInductionCore (induction x as pat using u) as IH)).
+  iInduction_ x xs Hs ltac:(fun _ => induction x as pat using u) IH.
 
 (** * Löb Induction *)
 Tactic Notation "iLöbCore" "as" constr (IH) :=
@@ -1851,20 +1826,27 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
      | _ => idtac
      end].
 
-Tactic Notation "iLöbRevert" constr(Hs) "with" tactic3(tac) :=
-  iRevertIntros Hs with (
-    iRevertIntros "∗" with tac
+Ltac iLöb0_ Hs IH :=
+  iRevertIntros0_ Hs ltac:(fun _ =>
+    iRevertIntros0_ "∗" ltac:(fun _ =>
+      iLöbCore as IH
+    )
+  ).
+Ltac iLöb_ xs Hs IH :=
+  iRevertIntros0_ Hs ltac:(fun _ =>
+    iRevertIntros_ xs "∗" ltac:(fun _ =>
+      iLöbCore as IH
+    )
   ).
 
 Tactic Notation "iLöb" "as" constr (IH) :=
-  iLöbRevert "" with (iLöbCore as IH).
+  iLöb0_ "" IH.
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ne_ident_list(xs) ")" :=
-  iLöbRevert "" with (iRevertIntros_ "" xs ltac:(idtac; iLöbCore as IH)).
-
+  iLöb_ xs "" IH.
 Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) :=
-  iLöbRevert Hs with (iLöbCore as IH).
+  iLöb0_ Hs IH.
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ne_ident_list(xs) ")" constr(Hs) :=
-  iLöbRevert Hs with (iRevertIntros_ "" xs ltac:(idtac; iLöbCore as IH)).
+  iLöb0_ xs Hs IH.
 
 (** * Assert *)
 (* The argument [p] denotes whether [Q] is persistent. It can either be a
@@ -2056,65 +2038,61 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
 
 (* Without closing view shift *)
 Tactic Notation "iInvCore" constr(N) "with" constr(pats) "in" tactic3(tac) :=
-  iInvCore N with pats as (@None string) in ltac:(tac).
+  iInvCore N with pats as (@None string) in tac.
 (* Without selection pattern *)
 Tactic Notation "iInvCore" constr(N) "as" constr(Hclose) "in" tactic3(tac) :=
-  iInvCore N with "[$]" as Hclose in ltac:(tac).
+  iInvCore N with "[$]" as Hclose in tac.
 (* Without both *)
 Tactic Notation "iInvCore" constr(N) "in" tactic3(tac) :=
-  iInvCore N with "[$]" as (@None string) in ltac:(tac).
+  iInvCore N with "[$]" as (@None string) in tac.
 
 (* With everything *)
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
-  iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as pat).
-Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" ne_simple_intropattern_list(xs) ")"
-    constr(pat) constr(Hclose) :=
+  iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp0_ H pat).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as"
+    "(" ne_simple_intropattern_list(xs) ")" constr(pat) constr(Hclose) :=
   iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp_ H xs pat).
 
 (* Without closing view shift *)
+Ltac iDestructAccAndHyp0 pat x H :=
+  lazymatch type of x with
+  | unit => destruct x as []; iDestructHyp0_ H pat
+  | _ => fail "Missing intro pattern for accessor variable"
+  end.
+
+Ltac iDestructAccAndHyp xs pat x H :=
+  let go := ltac2:(tac xs |-
+    match of_ltac1_list xs with
+    | [] =>
+      Control.throw_invalid_argument "iDestructAccAndHyp: List should be non-empty"
+    | x1 :: xs' =>
+      ltac1:(x1 |- intros x1) x1;
+      ltac1:(tac xs' |- tac xs') tac (Ltac1.of_list xs')
+    end) in
+  lazymatch type of x with
+  | unit => destruct x as []; iDestructHyp_ H xs pat
+  | _ => revert x; go ltac:(fun xs' => iDestructHyp_ H xs' pat) xs
+  end.
+
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) :=
-  iInvCore N with Hs in
-    (fun x H => lazymatch type of x with
-                | unit => destruct x as []; iDestructHyp H as pat
-                | _ => fail "Missing intro pattern for accessor variable"
-                end).
-Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" ne_simple_intropattern_list(xs) ")"
-    constr(pat) :=
-  iInvCore N with Hs in
-    (fun x H => lazymatch type of x with
-                | unit => destruct x as []; iDestructHyp_ H xs pat
-                | _ => revert x; iDestructHyp_intros_hd_ H xs pat
-                end).
+  iInvCore N with Hs in iDestructAccAndHyp0 pat.
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as"
+    "(" ne_simple_intropattern_list(xs) ")" constr(pat) :=
+  iInvCore N with Hs in iDestructAccAndHyp xs pat.
 
 (* Without selection pattern *)
 Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
-  iInvCore N as (Some Hclose) in
-    (fun x H => lazymatch type of x with
-                | unit => destruct x as []; iDestructHyp H as pat
-                | _ => fail "Missing intro pattern for accessor variable"
-                end).
+  iInvCore N as (Some Hclose) in iDestructAccAndHyp0 pat.
 Tactic Notation "iInv" constr(N) "as" "(" ne_simple_intropattern_list(xs) ")"
     constr(pat) constr(Hclose) :=
-  iInvCore N as (Some Hclose) in
-    (fun x H => lazymatch type of x with
-                | unit => destruct x as []; iDestructHyp_ H xs pat
-                | _ => revert x; iDestructHyp_intros_hd_ H xs pat
-                end).
+  iInvCore N as (Some Hclose) in iDestructAccAndHyp xs pat.
 
 (* Without both *)
 Tactic Notation "iInv" constr(N) "as" constr(pat) :=
-  iInvCore N in
-    (fun x H => lazymatch type of x with
-                | unit => destruct x as []; iDestructHyp H as pat
-                | _ => fail "Missing intro pattern for accessor variable"
-                end).
+  iInvCore N in iDestructAccAndHyp0 pat.
 Tactic Notation "iInv" constr(N) "as" "(" ne_simple_intropattern_list(xs) ")"
     constr(pat) :=
-  iInvCore N in
-    (fun x H => lazymatch type of x with
-                | unit => destruct x as []; iDestructHyp_ H xs pat
-                | _ => revert x; iDestructHyp_intros_hd_ H xs pat
-                end).
+  iInvCore N in iDestructAccAndHyp xs pat.
 
 (** Miscellaneous *)
 Tactic Notation "iAccu" :=
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index bc4e313ff4cb7cbf185f6684ccf2eed186c7a12d..e8bca07c1cf0eca433720c98852b06d892ac79ab 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -249,7 +249,8 @@ Tactic failure: wp_pure: "Hcred" is not fresh.
   I : val → Prop
   Heq : ∀ v : val, I v ↔ I #true
   ============================
-  ⊢ l ↦_(λ _ : val, I #true) □
+  --------------------------------------∗
+  l ↦_(λ _ : val, I #true) □
 "wp_iMod_fupd_atomic"
      : string
 2 goals