From c85c4541a2b7ebffe50b354e76b75d83c73d9848 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Wed, 11 Jan 2017 10:59:15 +0100
Subject: [PATCH] Rename tl_inG into na_inG.

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

diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 5837dcb68..68c7935bc 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -9,7 +9,7 @@ Import uPred.
 Definition na_inv_pool_name := gname.
 
 Class na_invG Σ :=
-  tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+  na_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
 
 Section defs.
   Context `{invG Σ, na_invG Σ}.
@@ -84,8 +84,8 @@ Section proofs.
     na_inv p N P -∗ na_own p F ={E}=∗ ▷ P ∗ na_own p (F∖↑N) ∗
                        (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F).
   Proof.
-    rewrite /na_inv. iIntros (??) "#Htlinv Htoks".
-    iDestruct "Htlinv" as (i) "[% Hinv]".
+    rewrite /na_inv. iIntros (??) "#Hnainv Htoks".
+    iDestruct "Hnainv" as (i) "[% Hinv]".
     rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
     rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
     iDestruct "Htoks" as "[[Htoki $] $]".
-- 
GitLab