From bb35dbf52dbd7b1b508e40aa66934cbd682297ed Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Jan 2017 20:30:05 +0100
Subject: [PATCH] solve_inG ftw

---
 theories/typing/adequacy.v | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/theories/typing/adequacy.v b/theories/typing/adequacy.v
index 6f2f7f04..7b4eff80 100644
--- a/theories/typing/adequacy.v
+++ b/theories/typing/adequacy.v
@@ -18,13 +18,7 @@ Class typePreG Σ := PreTypeG {
 Definition typeΣ : gFunctors :=
   #[heapΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
 Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
-Proof.
-  split.
-  - apply subG_heapPreG. solve_inG.
-  - apply subG_lftPreG. solve_inG.
-  - solve_inG.
-  - solve_inG.
-Qed.
+Proof. solve_inG. Qed.
 
 Section type_soundness.
   Definition exit_cont : val := λ: [<>], #().
-- 
GitLab