Commit 3077c6c6 authored by Ralf Jung's avatar Ralf Jung

more spacing fixes for better grouping

parent 59a8f5bf
Pipeline #2584 passed with stage
in 4 minutes and 13 seconds
......@@ -9,9 +9,8 @@ Class authG Σ (A : ucmraT) := AuthG {
auth_inG :> inG Σ (authR A);
auth_discrete :> CMRADiscrete A;
}.
(* The global functor we need and register that they match. *)
Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
Instance subG_authΣ Σ A : subG (authΣ A) Σ CMRADiscrete A authG Σ A.
Proof. intros ?%subG_inG ?. by split. Qed.
......
......@@ -5,9 +5,9 @@ Import uPred.
Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
saved_prop_inG :> inG Σ (agreeR (laterC (F (iPreProp Σ)))).
Definition savedPropΣ (F : cFunctor) : gFunctors :=
#[ GFunctor (agreeRF ( F)) ].
Instance subG_savedPropΣ {Σ F} : subG (savedPropΣ F) Σ savedPropG Σ F.
Proof. apply subG_inG. Qed.
......
......@@ -8,9 +8,8 @@ Class stsG Σ (sts : stsT) := StsG {
sts_inG :> inG Σ (stsR sts);
sts_inhabited :> Inhabited (sts.state sts);
}.
(* The global functor we need and register that they match. *)
Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (constRF (stsR sts)) ].
Instance subG_stsΣ Σ sts :
subG (stsΣ sts) Σ Inhabited (sts.state sts) stsG Σ sts.
Proof. intros ?%subG_inG ?. by split. Qed.
......
Markdown is supported
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