From 160b8c97e256265cbc44844c9a799be4bec094c1 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 17 Jun 2019 00:46:21 +0200
Subject: [PATCH] ltac_tactics.v: drop dead branch
---
theories/proofmode/ltac_tactics.v | 8 +-------
1 file changed, 1 insertion(+), 7 deletions(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index a6c6da970..15fb921b7 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1027,13 +1027,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
end in
lazymatch type of t with
| ident => iPoseProofCoreHyp t as Htmp; spec_tac (); [..|tac Htmp]
- | _ =>
- lazymatch eval compute in lazy_tc with
- | true =>
- iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
- | false =>
- iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
- end
+ | _ => iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
end.
(** * The apply tactic *)
--
GitLab