From e78dfb5f8ad95ceb971f822100ca6e68792e9211 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Mar 2017 20:48:16 +0100
Subject: [PATCH] Remove old debugging code.
---
theories/proofmode/tactics.v | 1 -
1 file changed, 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 2d7a50bc7..e5444b291 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -830,7 +830,6 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| false => go H pat; find_pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
- | _ => fail "hallo" pats
end in
let pats := intro_pat.parse pat in
find_pat false pats.
--
GitLab