From 477f0e9b4f6bb7321321e7e0e80eba823822bf3b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 9 Jan 2017 11:02:44 +0100
Subject: [PATCH] use solve_inG tactic

---
 theories/lang/adequacy.v         | 2 +-
 theories/lifetime/lifetime_sig.v | 6 +-----
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index e402dc73..2534ddfd 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -15,7 +15,7 @@ Definition heapΣ : gFunctors :=
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
-Proof. intros [? [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   (∀ `{heapG Σ}, {{ heap_ctx }} e {{ v, ⌜φ v⌝ }}) →
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 675899ed..aea0750c 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -61,11 +61,7 @@ Definition lftΣ : gFunctors :=
      GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
 Instance subG_stsΣ Σ :
   subG lftΣ Σ → lftPreG Σ.
-Proof.
-  intros [? [?%subG_inG [?%subG_inG [?%subG_inG [?%subG_inG
-             ?%subG_inG]%subG_inv]%subG_inv]%subG_inv]%subG_inv]%subG_inv.
-  split; first apply _; done.
-Qed.
+Proof. solve_inG. Qed.
 
 Module Type lifetime_sig.
   (** Definitions *)
-- 
GitLab