diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index c96710a0dbf86e19a08cc4e0707eb1f378bb8822..3f1f8557e19efa5507d24747dc19c56605c2721b 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -2046,14 +2046,6 @@ Tactic Notation "iInvCore" constr(N) "as" constr(Hclose) "in" tactic3(tac) :=
 Tactic Notation "iInvCore" constr(N) "in" tactic3(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 => 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
@@ -2074,6 +2066,14 @@ Ltac iDestructAccAndHyp xs pat x H :=
   | _ => revert x; go ltac:(fun xs' => iDestructHyp_ H xs' pat) xs
   end.
 
+(* With everything *)
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
+  iInvCore N with Hs as (Some Hclose) in iDestructAccAndHyp0 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 iDestructAccAndHyp xs pat.
+
+(* Without closing view shift *)
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) :=
   iInvCore N with Hs in iDestructAccAndHyp0 pat.
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as"
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 56243f168e05f00ba018d58b1414e190940b8cfb..7720a0607012189584a78da6389f5e9b1bab807a 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -139,9 +139,7 @@ Tactic failure: iInv: invariant "H2" not found.
 The command has indeed failed with message:
 Tactic failure: Missing intro pattern for accessor variable.
 The command has indeed failed with message:
-The command has not failed!
-The command has indeed failed with message:
-Tactic failure: iExistDestruct: cannot destruct (Φ H1).
+Tactic failure: Missing intro pattern for accessor variable.
 The command has indeed failed with message:
 Tactic failure: Missing intro pattern for accessor variable.
 The command has indeed failed with message:
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index a751684b0f41a9a9690391f2cfde72e8b0d07f07..6fe33fb78b95117c60b09cd705d62cd8cf277973 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -251,10 +251,9 @@ Section iris_tests.
       Fail iInv "HINV" as "HINVinner".
       iInv "HINV" as (b) "HINVinner"; rename b into b_exists. Undo.
       (* Both sel.pattern and closing view shift *)
-      (* FIXME this one is broken: no proper error message without a pattern for
-      the accessor variable, and an error when the pattern is given *)
-      Fail Fail iInv "HINV" with "[//]" as "HINVinner" "Hclose".
-      Fail iInv "HINV" with "[//]" as (b) "HINVinner" "Hclose"; rename b into b_exists.
+      Fail iInv "HINV" with "[//]" as "HINVinner" "Hclose".
+      iInv "HINV" with "[//]" as (b) "HINVinner" "Hclose";
+        rename b into b_exists. Undo.
       (* Sel.pattern but no closing view shift *)
       Fail iInv "HINV" with "[//]" as "HINVinner".
       iInv "HINV" with "[//]" as (b) "HINVinner"; rename b into b_exists. Undo.