This applies the PreG
change we did for gen_heap
in !585 (merged) to all PreG
classes, if possible. However, it turns out that this is not always possible, since some of these use a "mixin" style:
Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
ownP_invG : invG Σ;
ownP_inG :> inG Σ (excl_authR (stateO Λ));
ownP_name : gname;
}.
Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
ownPPre_invG :> invPreG Σ;
ownPPre_state_inG :> inG Σ (excl_authR (stateO Λ))
}.
Here, we cannot make ownPPreG
a field of ownPG
.