From b619294079c0d5e8f4fc1bf627865297d1d4a46d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Aug 2016 13:24:03 +0200
Subject: [PATCH] closed proofs: be more explicit about composed gFunctors

---
 tests/barrier_client.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 686c3810d..79bf4c9a9 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -57,10 +57,16 @@ Section client.
 Qed.
 End client.
 
+Section ClosedProofs.
+
+Definition Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
+
 Lemma client_adequate σ : adequate client σ (λ _, True).
 Proof.
-  apply (heap_adequacy #[ heapΣ ; barrierΣ ; spawnΣ ])=> ?.
+  apply (heap_adequacy Σ)=> ?.
   apply (client_safe (nroot .@ "barrier")); auto with ndisj.
 Qed.
 
 Print Assumptions client_adequate.
+
+End ClosedProofs.
-- 
GitLab