From 56f0afb23dc761c9a822a505d6d7d2cc435b681b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 7 Apr 2017 17:48:06 +0200
Subject: [PATCH] provide functor for cancellable invariants

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

diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 451fb5b0e..b2bbd5cba 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -5,6 +5,10 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
+Definition cinvΣ : gFunctors := #[GFunctor fracR].
+
+Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
+Proof. solve_inG. Qed.
 
 Section defs.
   Context `{invG Σ, cinvG Σ}.
-- 
GitLab