From 35ac5e8edcb3c2d066b13d75238ae3672260f774 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Feb 2016 10:03:52 +0100
Subject: [PATCH] barrier: strive for consistency between barrierGF and the
 inGF assumptions; also change some instance names

---
 barrier/barrier.v          | 6 +++---
 barrier/client.v           | 2 +-
 program_logic/saved_prop.v | 2 +-
 program_logic/sts.v        | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index e08d4bbed..c36779a22 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -125,14 +125,14 @@ End barrier_proto.
 Import barrier_proto.
 
 (* The functors we need. *)
-Definition barrierGFs : iFunctors := [stsGF sts; agreeF].
+Definition barrierGF : iFunctors := [stsGF sts; agreeF].
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
   Context {Σ : iFunctorG} (N : namespace).
   Context `{heapG Σ} (heapN : namespace).
-  Context `{stsG heap_lang Σ sts}.
-  Context `{savedPropG heap_lang Σ}.
+  (* These are exactly the elements of barrierGF *)
+  Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}.
 
   Local Hint Immediate i_states_closed low_states_closed : sts.
   Local Hint Resolve signal_step wait_step split_step : sts.
diff --git a/barrier/client.v b/barrier/client.v
index 5db27c178..3db716f0f 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -26,7 +26,7 @@ Section client.
 End client.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := #[ heapGF ; barrierGFs ].
+  Definition Σ : iFunctorG := #[ heapGF ; barrierGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index fa0119211..ee573c934 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -5,7 +5,7 @@ Import uPred.
 Notation savedPropG Λ Σ :=
   (inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
 
-Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
+Instance inGF_savedPropG `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
 Proof. apply: inGF_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Λ Σ}
diff --git a/program_logic/sts.v b/program_logic/sts.v
index a2716da5c..b66a60e13 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -9,7 +9,7 @@ Class stsG Λ Σ (sts : stsT) := StsG {
 Coercion sts_inG : stsG >-> inG.
 
 Definition stsGF (sts : stsT) : iFunctor := constF (stsRA sts).
-Instance stsGF_inGF sts `{inGF Λ Σ (stsGF sts)}
+Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
   `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
 Proof. split; try apply _. apply: inGF_inG. Qed.
 
-- 
GitLab