Skip to content
Snippets Groups Projects
Commit 92b3c168 authored by Yusuke Matsushita's avatar Yusuke Matsushita Committed by Jacques-Henri Jourdan
Browse files

modify typeG and type_preG component names

parent 58bfc65c
No related branches found
No related tags found
No related merge requests found
......@@ -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 :=
......
......@@ -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 Σ
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment