From 9fa0b57d44cbba40d7bb272b45cc0875bc68940d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Wed, 11 Jan 2017 16:05:17 +0100
Subject: [PATCH] =?UTF-8?q?Renaming=20again=20[na=5FinG]=20and=20adding=20?=
 =?UTF-8?q?[na=5Finv=CE=A3]=20and=20[subG=5Fna=5FinvG].?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 68c7935bc..6f760c91e 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -9,7 +9,11 @@ Import uPred.
 Definition na_inv_pool_name := gname.
 
 Class na_invG Σ :=
-  na_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+  na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+Definition na_invΣ : gFunctors :=
+  #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
+Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
+Proof. solve_inG. Qed.
 
 Section defs.
   Context `{invG Σ, na_invG Σ}.
-- 
GitLab