From 381e85094249544aa72b297311bf71446d494e8c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 13 Jun 2017 10:50:19 +0200
Subject: [PATCH] =?UTF-8?q?Let=20always=5Fidemp=20be=20the=20rule=20`?=
 =?UTF-8?q?=E2=96=A1=20=E2=96=A1=20P=20=E2=8A=A3=E2=8A=A2=20=E2=96=A1=20P`?=
 =?UTF-8?q?=20in=20both=20ways.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/derived.v   | 4 ++--
 theories/base_logic/primitive.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index cc6f3af30..629d54ccf 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -478,9 +478,9 @@ Global Instance always_flip_mono' :
 Proof. intros P Q; apply always_mono. Qed.
 
 Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
-Proof. intros <-. apply always_idemp. Qed.
+Proof. intros <-. apply always_idemp_2. Qed.
 Lemma always_idemp P : □ □ P ⊣⊢ □ P.
-Proof. apply (anti_symm _); auto using always_idemp. Qed.
+Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
 
 Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. apply (anti_symm _); auto using always_pure_2. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 16d109fe8..0b84b8d59 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -427,7 +427,7 @@ Proof.
   unseal; split=> n x ? /=.
   eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
 Qed.
-Lemma always_idemp P : □ P ⊢ □ □ P.
+Lemma always_idemp_2 P : □ P ⊢ □ □ P.
 Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
 
 Lemma always_pure_2 φ : ⌜φ⌝ ⊢ □ ⌜φ⌝.
-- 
GitLab