Version of `iEval ... in ...`.

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.

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) :=