Fix bug in `iInv`.

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"

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:

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.