From f197e42d63afeda982a0ac32d354c8b0ab738b78 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 31 Dec 2017 18:28:54 +0100
Subject: [PATCH] Version of `iEval ... in ...`.

---
 theories/proofmode/coq_tactics.v | 11 +++++++++++
 theories/proofmode/tactics.v     |  9 +++++++++
 2 files changed, 20 insertions(+)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 124ae4a41..ac28a1a1b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -418,6 +418,17 @@ Lemma tac_eval Δ Q Q' :
   envs_entails Δ Q' → envs_entails Δ Q.
 Proof. by intros <-. Qed.
 
+Lemma tac_eval_in Δ Δ' i p P P' Q :
+  envs_lookup i Δ = Some (p, P) →
+  (P ⊢ P') →
+  envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' →
+  envs_entails Δ' Q → envs_entails Δ Q.
+Proof.
+  rewrite /envs_entails. intros ? HP ? <-.
+  rewrite envs_simple_replace_sound //; simpl.
+  by rewrite HP right_id wand_elim_r.
+Qed.
+
 Lemma tac_assumption Δ i p P Q :
   envs_lookup i Δ = Some (p,P) → FromAssumption p P Q →
   envs_entails Δ Q.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 0dd09eebe..a894b9475 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -85,7 +85,16 @@ Tactic Notation "iEval" tactic(t) :=
   iStartProof;
   eapply tac_eval; [t; reflexivity|].
 
+Tactic Notation "iEval" tactic(t) "in" constr(H) :=
+  iStartProof;
+  eapply tac_eval_in with _ H _ _ _;
+    [env_reflexivity || fail "iEval:" H "not found"
+    |t; reflexivity
+    |env_reflexivity
+    |].
+
 Tactic Notation "iSimpl" := iEval simpl.
+Tactic Notation "iSimpl" "in" constr(H) := iEval simpl in H.
 
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
-- 
GitLab