diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 11ca3016c3a879cddd72da7f05b6d2dcc0702754..19db5a773733508f916ce8098ca1ea8535ae35dd 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -948,6 +948,9 @@ Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
   iDestructCore lem as false (fun H =>
     iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
+Tactic Notation "iVs" open_constr(lem) "as" "%" simple_intropattern(pat) :=
+  iDestructCore lem as false (fun H => iVsCore H; iPure H as pat).
+
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
 Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.