From aa897a41b0f56dd74d7e2ae12fe63aab25fb465b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Feb 2016 12:26:37 +0100
Subject: [PATCH] avoid a pitfall by not tying barrierG to heapG at all

---
 barrier/barrier.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index d610b5ba3..9b24d5d0f 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -126,20 +126,20 @@ Import barrier_proto.
 
 (** The monoids we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
-Class barrierG Σ `{heapG Σ} := BarrierG {
+Class barrierG Σ := BarrierG {
   barrier_stsG :> stsG heap_lang Σ sts;
   barrier_savedPropG :> savedPropG heap_lang Σ;
 }.
 
 Definition barrierGF : iFunctors := [stsGF sts; agreeF].
 
-Instance inGF_barrierG `{heapG Σ} `{inGF heap_lang Σ (stsGF sts)}
+Instance inGF_barrierG `{inGF heap_lang Σ (stsGF sts)}
          `{inGF heap_lang Σ agreeF} : barrierG Σ.
 Proof. split; apply _. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-  Context {Σ : iFunctorG} `{barrierG Σ}.
+  Context {Σ : iFunctorG} `{!heapG Σ} `{!barrierG Σ}.
   Context (N : namespace) (heapN : namespace).
 
   Local Hint Immediate i_states_closed low_states_closed : sts.
-- 
GitLab