From cea60198e9c4b82a41e70369f766b0beaee624c9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Mar 2018 12:59:52 +0100
Subject: [PATCH] Coq future-compat: use qualified name for

---
 theories/proofmode/coq_tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 077044c59..4cab6ec0e 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -92,7 +92,7 @@ Definition envs_simple_replace {M} (i : ident) (p : bool) (Γ : env (uPred M))
 
 Definition envs_replace {M} (i : ident) (p q : bool) (Γ : env (uPred M))
     (Δ : envs M) : option (envs M) :=
-  if eqb p q then envs_simple_replace i p Γ Δ
+  if Bool.eqb p q then envs_simple_replace i p Γ Δ
   else envs_app q Γ (envs_delete i p Δ).
 
 Definition env_spatial_is_nil {M} (Δ : envs M) :=
@@ -285,7 +285,7 @@ Lemma envs_replace_sound' Δ Δ' i p q Γ :
   envs_replace i p q Γ Δ = Some Δ' →
   of_envs (envs_delete i p Δ) ⊢ □?q [∗] Γ -∗ of_envs Δ'.
 Proof.
-  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
+  rewrite /envs_replace; destruct (Bool.eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
   - apply envs_app_sound.
 Qed.
-- 
GitLab