Commit 2c01bead authored by Joseph Tassarotti's avatar Joseph Tassarotti

Fix build on Coq master.

parent 353be255
......@@ -553,7 +553,7 @@ Qed.
Lemma tac_frame_pure Δ (φ : Prop) P Q :
φ Frame true ⌜φ⌝ P Q envs_entails Δ Q envs_entails Δ P.
Proof.
rewrite envs_entails_eq => ?? ->. rewrite -(frame _ ⌜φ⌝ P) /=.
rewrite envs_entails_eq => ? Hframe ->. rewrite -Hframe /=.
rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
auto using and_intro, pure_intro.
Qed.
......@@ -563,8 +563,8 @@ Lemma tac_frame Δ Δ' i p R P Q :
Frame p R P Q
envs_entails Δ' Q envs_entails Δ P.
Proof.
rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ? HQ.
rewrite (envs_lookup_sound' _ false) //. by rewrite -(frame _ R P) HQ.
rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hframe HQ.
rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
Qed.
(** * Disjunction *)
......
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