From 467b118b3e4e0c2c3c8a2a3ced6ea7c0d459fa77 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 31 Dec 2017 18:27:29 +0100
Subject: [PATCH] Use entailment in `iEval` so that setoid rewriting works.

---
 theories/proofmode/coq_tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 121102ce2..124ae4a41 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -414,9 +414,9 @@ Qed.
 
 (** * Basic rules *)
 Lemma tac_eval Δ Q Q' :
-  Q = Q' →
+  (Q' ⊢ Q) →
   envs_entails Δ Q' → envs_entails Δ Q.
-Proof. by intros ->. Qed.
+Proof. by intros <-. Qed.
 
 Lemma tac_assumption Δ i p P Q :
   envs_lookup i Δ = Some (p,P) → FromAssumption p P Q →
-- 
GitLab