From aaa9eb9c50ef99c7ee9ccbe253e31ff8c7230a0c Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 2 Mar 2022 00:55:00 +0100
Subject: [PATCH] Style fixes from review

---
 docs/resource_algebras.md                   | 3 ++-
 iris/base_logic/lib/cancelable_invariants.v | 3 ++-
 iris/base_logic/lib/gset_bij.v              | 2 +-
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 1c32b743b..55c472ae6 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -275,8 +275,9 @@ your example would look as follows:
 
 ```coq
 Class libG Σ := { lib_inG : inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
-Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
 Local Existing Instance lib_inG.
+
+Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
 Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
 Proof. solve_inG. Qed.
 ```
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 2515ed6be..8273c0797 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -6,9 +6,10 @@ From iris.prelude Require Import options.
 Import uPred.
 
 Class cinvG Σ := cinv_inG : inG Σ fracR.
-Definition cinvΣ : gFunctors := #[GFunctor fracR].
 Local Existing Instance cinv_inG.
 
+Definition cinvΣ : gFunctors := #[GFunctor fracR].
+
 Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index 9be5df415..402144c42 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -29,8 +29,8 @@ From iris.prelude Require Import options.
 (* The uCMRA we need. *)
 Class gset_bijG Σ A B `{Countable A, Countable B} :=
   GsetBijG { gset_bijG_inG : inG Σ (gset_bijR A B); }.
-Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
 Local Existing Instance gset_bijG_inG.
+Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
 
 Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
   #[ GFunctor (gset_bijR A B) ].
-- 
GitLab