From d8edb4e8665787b8fdc8170f3210b7d47578fceb Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 25 May 2019 13:28:38 +0200 Subject: [PATCH] flat combiner: use solve_inG --- theories/logatom/flat_combiner/atomic_sync.v | 2 +- theories/logatom/flat_combiner/flat.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/logatom/flat_combiner/atomic_sync.v b/theories/logatom/flat_combiner/atomic_sync.v index a01dc87..bf1b078 100644 --- a/theories/logatom/flat_combiner/atomic_sync.v +++ b/theories/logatom/flat_combiner/atomic_sync.v @@ -11,7 +11,7 @@ Class syncG Σ := sync_tokG :> inG Σ syncR. Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)]. Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ. -Proof. by intros ?%subG_inG. Qed. +Proof. solve_inG. Qed. Section atomic_sync. Context `{EqDecision A, !heapG Σ, !lockG Σ}. diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v index 257689f..a4dd724 100644 --- a/theories/logatom/flat_combiner/flat.v +++ b/theories/logatom/flat_combiner/flat.v @@ -58,7 +58,7 @@ Definition flatΣ : gFunctors := savedPredΣ val ]. Instance subG_flatΣ {Σ} : subG flatΣ Σ → flatG Σ. -Proof. intros [?%subG_inG [? _]%subG_inv]%subG_inv. split; apply _. Qed. +Proof. solve_inG. Qed. Section proof. Context `{!heapG Σ, !lockG Σ, !flatG Σ} (N: namespace). -- GitLab