Commit 10fe1509 authored by Joseph Tassarotti's avatar Joseph Tassarotti

Fix build on Coq master.

parent 778291fc
......@@ -357,8 +357,8 @@ Lemma tac_specialize_assert_pure Δ j q R P1 P2 φ Q :
envs_entails Δ Q.
Proof.
destruct envs_simple_replace as [Δ'|] eqn:?; last by (intros; exfalso).
rewrite envs_entails_eq=> ?????. rewrite envs_simple_replace_singleton_sound //=.
rewrite -intuitionistically_if_idemp into_wand /= -(from_pure true P1) /bi_intuitionistically.
rewrite envs_entails_eq=> ? Hwand ???. rewrite envs_simple_replace_singleton_sound //=.
rewrite -intuitionistically_if_idemp Hwand /= -(from_pure true P1) /bi_intuitionistically.
rewrite pure_True //= persistently_affinely_elim persistently_pure
affinely_True_emp affinely_emp.
by rewrite emp_wand wand_elim_r.
......@@ -622,7 +622,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.
......@@ -637,9 +637,9 @@ Lemma tac_frame Δ i P Q :
envs_entails Δ P.
Proof.
destruct envs_lookup_delete as [((p&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
rewrite envs_entails_eq. intros (HQ&Heq).
rewrite envs_entails_eq. intros (Hframe&Heq).
apply envs_lookup_delete_Some in Hlookup as (?&->).
rewrite (envs_lookup_sound' _ false) //. by rewrite -(frame _ R P) Heq.
rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe Heq.
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