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

Also hide ghost_mapG instances

parent 3f934cbe
Pipeline #63442 passed with stage
in 12 minutes and 44 seconds
......@@ -66,11 +66,11 @@ these can be matched up with the invariant namespaces. *)
(** The CMRAs we need, and the global ghost names we are using. *)
Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heapGpreS_heap :> ghost_mapG Σ L V;
gen_heapGpreS_meta :> ghost_mapG Σ L gname;
gen_heapGpreS_heap : ghost_mapG Σ L V;
gen_heapGpreS_meta : ghost_mapG Σ L gname;
gen_heapGpreS_meta_data : inG Σ (reservation_mapR (agreeR positiveO));
}.
Local Existing Instance gen_heapGpreS_meta_data.
Local Existing Instances gen_heapGpreS_meta_data gen_heapGpreS_heap gen_heapGpreS_meta.
Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
gen_heap_inG :> gen_heapGpreS L V Σ;
......
......@@ -9,8 +9,9 @@ Definition proph_val_list (P V : Type) := list (P * V).
(** The CMRA we need. *)
Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
proph_map_GpreS_inG :> ghost_mapG Σ P (list V)
proph_map_GpreS_inG : ghost_mapG Σ P (list V)
}.
Local Existing Instances proph_map_GpreS_inG.
Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapGS {
proph_map_inG :> proph_mapGpreS P V Σ;
......
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