From 6a4c627965baede995ab75d70c9af7fb3a69df84 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 11 Nov 2017 11:03:46 +0100
Subject: [PATCH] add later_ne; make later_proper match the other _proper
 lemmas

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

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index c6c897cbe..35c2e3f5f 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -672,9 +672,9 @@ Proof.
 Qed.
 
 (* Later derived *)
-Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
+Lemma later_proper' P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
 Proof. by intros ->. Qed.
-Hint Resolve later_mono later_proper.
+Hint Resolve later_mono later_proper'.
 Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M).
 Proof. intros P Q; apply later_mono. Qed.
 Global Instance later_flip_mono' :
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 6796f5a44..46768bd2e 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -307,7 +307,8 @@ Proof.
   unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
   apply HPQ; eauto using cmra_validN_S.
 Qed.
-Global Instance later_proper' :
+Definition later_ne : NonExpansive (@uPred_later M) := _.
+Global Instance later_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
 Global Instance plainly_ne : NonExpansive (@uPred_plainly M).
 Proof.
-- 
GitLab