From cd5096b7950f064fba945ab7bece9587f38c5c47 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 May 2016 20:39:20 +0200
Subject: [PATCH] Fix bug in iDestruct "H" as %intro_pat.
---
proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 7f3d22d44..8fad7e786 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -515,7 +515,7 @@ Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
- let Htmp := iFresh in iDestruct H as Htmp; iPure Htmp as pat.
+ let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat.
(** * Always *)
Tactic Notation "iAlways":=
--
GitLab