Commit 467b118b authored by Robbert Krebbers's avatar Robbert Krebbers

Use entailment in `iEval` so that setoid rewriting works.

parent e374f84c
......@@ -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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment