From 13040135a505b58654f421a2066bdd6fc943b5a1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Jun 2018 13:27:09 +0200
Subject: [PATCH] re-state and not just register ownM_ne, cmra_valid_ne

---
 theories/base_logic/bi.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 3b7ce4c72..1b7fdb09d 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -167,8 +167,9 @@ Implicit Types A : Type.
 Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
-Global Existing Instance uPred_primitive.ownM_ne.
-Global Existing Instance uPred_primitive.cmra_valid_ne.
+Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
+Global Instance cmra_valid_ne {A : cmraT} : NonExpansive (@uPred_cmra_valid M A)
+  := uPred_primitive.cmra_valid_ne.
 
 (** Re-exporting primitive Own and valid lemmas *)
 Lemma ownM_op (a1 a2 : M) :
-- 
GitLab