Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

program_logic/auth.v

@@ -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.
 

program_logic/saved_prop.v

@@ -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.
 

program_logic/sts.v

@@ -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.