From 01984d7c103ec759a48496fa2a15a38a9477eb69 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Feb 2016 12:25:09 +0100
Subject: [PATCH] consistently use the inG and inGF pattern for the barrier

---
 barrier/barrier.v | 22 ++++++++++++++--------
 barrier/client.v  |  6 ++----
 2 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index e473a9cc6..d610b5ba3 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -124,15 +124,23 @@ End barrier_proto.
    the module into our namespaces. But Coq doesn't seem to support that...?? *)
 Import barrier_proto.
 
-(* The functors we need. *)
+(** The monoids we need. *)
+(* Not bundling heapG, as it may be shared with other users. *)
+Class barrierG Σ `{heapG Σ} := 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)}
+         `{inGF heap_lang Σ agreeF} : barrierG Σ.
+Proof. split; apply _. Qed.
+
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-  Context {Σ : iFunctorG} (N : namespace).
-  Context `{heapG Σ} (heapN : namespace).
-  (* These are exactly the elements of barrierGF *)
-  Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}.
+  Context {Σ : iFunctorG} `{barrierG Σ}.
+  Context (N : namespace) (heapN : namespace).
 
   Local Hint Immediate i_states_closed low_states_closed : sts.
   Local Hint Resolve signal_step wait_step split_step : sts.
@@ -477,9 +485,7 @@ Section proof.
 End proof.
 
 Section spec.
-  Context {Σ : iFunctorG}.
-  Context `{heapG Σ}.
-  Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}.
+  Context {Σ : iFunctorG} `{!heapG Σ} `{!barrierG Σ}. 
 
   Local Notation iProp := (iPropG heap_lang Σ).
 
diff --git a/barrier/client.v b/barrier/client.v
index 7726105ce..c1e88af81 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -5,10 +5,8 @@ Import uPred.
 Definition client := (let: "b" := newchan '() in wait "b")%L.
 
 Section client.
-  Context {Σ : iFunctorG} (N : namespace).
-  Context `{heapG Σ} (heapN : namespace).
-  (* TODO: This should be abstracted away somehow. *)
-  Context `{inGF heap_lang Σ (stsGF barrier_proto.sts)} `{inGF heap_lang Σ agreeF}.
+  Context {Σ : iFunctorG} `{!heapG Σ} `{!barrierG Σ}.
+  Context (N : namespace) (heapN : namespace).
 
   Local Notation iProp := (iPropG heap_lang Σ).
 
-- 
GitLab