use beq instead of Bool.eqb in envs_replace

theories/proofmode/coq_tactics.v

@@ -208,7 +208,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 Δ'.
 Proof.
-  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.
 Qed.
@@ -612,7 +612,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.
 Qed.
 

theories/proofmode/environments.v

@@ -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 :=