diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 121102ce20fcf089cff9176cc4d5fb6f7220fce1..124ae4a4107fe6e8fe6503301e1e64777f4c5d8c 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 →