From 1b56406c131a01f849727c65298b8113a2635e69 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Aug 2016 13:58:29 +0200
Subject: [PATCH] clarify inG comment; fix subG instance name

---
 program_logic/ghost_ownership.v | 2 +-
 program_logic/model.v           | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 0bbd38a5e..1f9e4859c 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -4,7 +4,7 @@ Import uPred.
 
 (** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
 [Σ]. This class is similar to the [subG] class, but written down in terms of
-individual CMRAs instead of lists of CMRA functors. This additional class is
+individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
 needed because Coq is otherwise unable to solve type class constraints due to
 higher-order unification problems. *)
 Class inG (Σ : gFunctors) (A : cmraT) :=
diff --git a/program_logic/model.v b/program_logic/model.v
index 789c57a5b..117809723 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -101,7 +101,7 @@ Proof.
   move=> H i; move: H=> /(_ i) [j ?].
   exists (Fin.L _ j). by rewrite /= fin_plus_inv_L.
 Qed.
-Instance inGF_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
+Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
 Proof.
   move=> H i; move: H=> /(_ i) [j ?].
   exists (Fin.R _ j). by rewrite /= fin_plus_inv_R.
-- 
GitLab