From ee15994e1b2763805ff38a4e2eb7fdbbda48b8b1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Sep 2016 16:07:52 +0200
Subject: [PATCH] Elimination of pure facts using Coq introduction patterns for
 iVs.

---
 proofmode/tactics.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 11ca3016c..19db5a773 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.
-- 
GitLab