Unverified Commit 51e6914e authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Hide preG instances

parent d0f86960
Pipeline #63453 passed with stage
in 7 minutes and 23 seconds
...@@ -73,10 +73,11 @@ Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := { ...@@ -73,10 +73,11 @@ Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
Local Existing Instances gen_heapGpreS_meta_data gen_heapGpreS_heap gen_heapGpreS_meta. Local Existing Instances gen_heapGpreS_meta_data gen_heapGpreS_heap gen_heapGpreS_meta.
Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS { Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
gen_heap_inG :> gen_heapGpreS L V Σ; gen_heap_inG : gen_heapGpreS L V Σ;
gen_heap_name : gname; gen_heap_name : gname;
gen_meta_name : gname gen_meta_name : gname
}. }.
Local Existing Instance gen_heap_inG.
Global Arguments GenHeapGS L V Σ {_ _ _} _ _. Global Arguments GenHeapGS L V Σ {_ _ _} _ _.
Global Arguments gen_heap_name {L V Σ _ _} _ : assert. Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
Global Arguments gen_meta_name {L V Σ _ _} _ : assert. Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
......
...@@ -36,9 +36,10 @@ Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := { ...@@ -36,9 +36,10 @@ Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
Local Existing Instance inv_heapGpreS_inG. Local Existing Instance inv_heapGpreS_inG.
Class inv_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG { Class inv_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
inv_heap_inG :> inv_heapGpreS L V Σ; inv_heap_inG : inv_heapGpreS L V Σ;
inv_heap_name : gname inv_heap_name : gname
}. }.
Local Existing Instance inv_heap_inG.
Global Arguments Inv_HeapG _ _ {_ _ _ _}. Global Arguments Inv_HeapG _ _ {_ _ _ _}.
Global Arguments inv_heap_name {_ _ _ _ _} _ : assert. Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
......
...@@ -14,10 +14,11 @@ Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := { ...@@ -14,10 +14,11 @@ Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
Local Existing Instances proph_map_GpreS_inG. Local Existing Instances proph_map_GpreS_inG.
Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapGS { Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapGS {
proph_map_inG :> proph_mapGpreS P V Σ; proph_map_inG : proph_mapGpreS P V Σ;
proph_map_name : gname proph_map_name : gname
}. }.
Global Arguments proph_map_name {_ _ _ _ _} _ : assert. Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
Local Existing Instances proph_map_inG.
Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors := Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
#[ghost_mapΣ P (list V)]. #[ghost_mapΣ P (list V)].
......
...@@ -15,7 +15,7 @@ Module invGS. ...@@ -15,7 +15,7 @@ Module invGS.
}. }.
Class invGS (Σ : gFunctors) : Set := InvG { Class invGS (Σ : gFunctors) : Set := InvG {
inv_inG :> invGpreS Σ; inv_inG : invGpreS Σ;
invariant_name : gname; invariant_name : gname;
enabled_name : gname; enabled_name : gname;
disabled_name : gname; disabled_name : gname;
...@@ -30,6 +30,7 @@ Module invGS. ...@@ -30,6 +30,7 @@ Module invGS.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
End invGS. End invGS.
Import invGS. Import invGS.
Local Existing Instances inv_inG.
Local Existing Instances invGpreS_inv invGpreS_enabled invGpreS_disabled. Local Existing Instances invGpreS_inv invGpreS_enabled invGpreS_disabled.
Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) := Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment