From 92b3c1681a154a3da47dd13c5adef8bdfcefdc95 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com>
Date: Sun, 28 Feb 2021 23:43:16 +0900
Subject: [PATCH] modify typeG and type_preG component names

---
 theories/typing/soundness.v | 6 +++---
 theories/typing/type.v      | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 7f3fa099..c2cfca78 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -8,10 +8,10 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Class typePreG Σ := PreTypeG {
-  type_heapG :> lrustPreG Σ;
-  type_lftG :> lftPreG Σ;
+  type_preG_lrustG :> lrustPreG Σ;
+  type_preG_lftG :> lftPreG Σ;
   type_preG_na_invG :> na_invG Σ;
-  type_frac_borrowG :> frac_borG Σ
+  type_preG_frac_borG :> frac_borG Σ
 }.
 
 Definition typeΣ : gFunctors :=
diff --git a/theories/typing/type.v b/theories/typing/type.v
index a943dab5..2cecc1eb 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -7,7 +7,7 @@ From lrust.typing Require Import lft_contexts.
 Set Default Proof Using "Type".
 
 Class typeG Σ := TypeG {
-  type_heapG :> lrustG Σ;
+  type_lrustG :> lrustG Σ;
   type_lftG :> lftG Σ;
   type_na_invG :> na_invG Σ;
   type_frac_borrowG :> frac_borG Σ
-- 
GitLab