diff --git a/tests/barrier_client.v b/tests/barrier_client.v index 686c3810d736561623d70d39253d274157bdfa76..79bf4c9a9b6f21197a10822c78c821c2902e7c34 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.