From 14a67809315df6d21f46e88a2046a905dcead8bd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2017 12:30:35 +0100
Subject: [PATCH] Prove pure_ne to make f_equiv work better.

---
 theories/base_logic/primitive.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index dce4435eb..12a444c59 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -211,8 +211,11 @@ Arguments uPred_holds {_} !_ _ _ /.
 Hint Immediate uPred_in_entails.
 
 (** Non-expansiveness and setoid morphisms *)
-Global Instance pure_proper : Proper (iff ==> (⊣⊢)) (@uPred_pure M).
+Global Instance pure_proper : Proper (iff ==> (⊣⊢)) (@uPred_pure M) | 0.
 Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ. Qed.
+Global Instance pure_ne n : Proper (iff ==> dist n) (@uPred_pure M) | 1.
+Proof. by intros φ1 φ2 ->. Qed.
+
 Global Instance and_ne : NonExpansive2 (@uPred_and M).
 Proof.
   intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
-- 
GitLab