From 2e2e756b2e05d03ef25fb5ce52a4897a800e1416 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 22 Mar 2017 13:20:51 +0100
Subject: [PATCH] Prove missing proper instances for inv

---
 theories/base_logic/lib/invariants.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 7ca2fc144..8866a4d18 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -25,6 +25,12 @@ Proof.
   rewrite inv_eq=> n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive.
 Qed.
 
+Global Instance inv_ne N : NonExpansive (inv N).
+Proof. apply contractive_ne, _. Qed.
+
+Global Instance inv_Proper N : Proper ((⊣⊢) ==> (⊣⊢)) (inv N).
+Proof. apply ne_proper, _. Qed.
+
 Global Instance inv_persistent N P : PersistentP (inv N P).
 Proof. rewrite inv_eq /inv; apply _. Qed.
 
-- 
GitLab