From 72ac1ee1c7d925f36433d8a15e1286f8f069dc1a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Mar 2018 09:11:45 +0100
Subject: [PATCH] =?UTF-8?q?absorbingly=5Fand=20=E2=86=92=20absorbingly=5Fa?=
 =?UTF-8?q?nd=5F1?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index e55ac337d..9d16b92fc 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -584,7 +584,7 @@ Proof.
 Qed.
 Lemma absorbingly_or P Q : <absorb> (P ∨ Q) ⊣⊢ <absorb> P ∨ <absorb> Q.
 Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
-Lemma absorbingly_and P Q : <absorb> (P ∧ Q) ⊢ <absorb> P ∧ <absorb> Q.
+Lemma absorbingly_and_1 P Q : <absorb> (P ∧ Q) ⊢ <absorb> P ∧ <absorb> Q.
 Proof. apply and_intro; apply absorbingly_mono; auto. Qed.
 Lemma absorbingly_forall {A} (Φ : A → PROP) : <absorb> (∀ a, Φ a) ⊢ ∀ a, <absorb> (Φ a).
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
@@ -1166,7 +1166,7 @@ Proof. rewrite /bi_affinely. apply _. Qed.
 Global Instance pure_absorbing φ : Absorbing (⌜φ⌝%I : PROP).
 Proof. by rewrite /Absorbing absorbingly_pure. Qed.
 Global Instance and_absorbing P Q : Absorbing P → Absorbing Q → Absorbing (P ∧ Q).
-Proof. intros. by rewrite /Absorbing absorbingly_and !absorbing. Qed.
+Proof. intros. by rewrite /Absorbing absorbingly_and_1 !absorbing. Qed.
 Global Instance or_absorbing P Q : Absorbing P → Absorbing Q → Absorbing (P ∨ Q).
 Proof. intros. by rewrite /Absorbing absorbingly_or !absorbing. Qed.
 Global Instance forall_absorbing {A} (Φ : A → PROP) :
-- 
GitLab