Commit f02bf0d6 authored by Ralf Jung's avatar Ralf Jung

use beq instead of Bool.eqb in envs_replace

parent d09d69d7
......@@ -203,7 +203,7 @@ Lemma envs_replace_sound' Δ Δ' i p q Γ :
envs_replace i p q Γ Δ = Some Δ'
of_envs (envs_delete true i p Δ) (if q then [] Γ else [] Γ) - of_envs Δ'.
rewrite /envs_replace; destruct (Bool.eqb _ _) eqn:Hpq.
rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
- apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
- apply envs_app_sound.
......@@ -607,7 +607,6 @@ Proof.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_singleton_sound Δ2) //; simpl.
rewrite HP1 into_wand /= -(add_modal P1' P1 Q). cancel [P1'].
apply wand_intro_l. by rewrite assoc !wand_elim_r.
......@@ -299,7 +299,7 @@ Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
(Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
if Bool.eqb p q then envs_simple_replace i p Γ Δ
if beq p q then envs_simple_replace i p Γ Δ
else envs_app q Γ (envs_delete true i p Δ).
Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
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