From e2882b61d6671218432acf93adb53b9d89c25e72 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 24 Feb 2017 20:31:47 +0100
Subject: [PATCH] Support envs_lookup_delete in internal iAssumptionCore
tactic.
---
theories/proofmode/tactics.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index cd4b76020..625970eee 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -122,6 +122,10 @@ Tactic Notation "iAssumptionCore" :=
first [is_evar i; fail 1 | env_cbv; reflexivity]
| |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
is_evar i; first [find Γp i P | find Γs i P]; env_cbv; reflexivity
+ | |- envs_lookup_delete ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+ first [is_evar i; fail 1 | env_cbv; reflexivity]
+ | |- envs_lookup_delete ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+ is_evar i; first [find Γp i P | find Γs i P]; env_cbv; reflexivity
end.
Tactic Notation "iAssumption" :=
--
GitLab