Commit d8edb4e8 by Ralf Jung

### flat combiner: use solve_inG

parent 2d6aa0bd
 ... @@ -11,7 +11,7 @@ Class syncG Σ := sync_tokG :> inG Σ syncR. ... @@ -11,7 +11,7 @@ Class syncG Σ := sync_tokG :> inG Σ syncR. Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)]. Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)]. Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ. Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ. Proof. by intros ?%subG_inG. Qed. Proof. solve_inG. Qed. Section atomic_sync. Section atomic_sync. Context `{EqDecision A, !heapG Σ, !lockG Σ}. Context `{EqDecision A, !heapG Σ, !lockG Σ}. ... ...
 ... @@ -58,7 +58,7 @@ Definition flatΣ : gFunctors := ... @@ -58,7 +58,7 @@ Definition flatΣ : gFunctors := savedPredΣ val ]. savedPredΣ val ]. Instance subG_flatΣ {Σ} : subG flatΣ Σ → flatG Σ. Instance subG_flatΣ {Σ} : subG flatΣ Σ → flatG Σ. Proof. intros [?%subG_inG [? _]%subG_inv]%subG_inv. split; apply _. Qed. Proof. solve_inG. Qed. Section proof. Section proof. Context `{!heapG Σ, !lockG Σ, !flatG Σ} (N: namespace). Context `{!heapG Σ, !lockG Σ, !flatG Σ} (N: namespace). ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!